Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456 Jaroslav Sevcik's Homepage
Jaroslav Ševčík
Currently a researcher at the University of Cambridge
(my CV)
Address
Room FS16
University of Cambridge
William Gates Building
15 JJ Thomson Avenue
Cambridge
CB3 0FD
My research interests are programming languages, concurrency, relaxed memory models, programming language semantics, and proof-carrying code.
Currently I am working on a certified compiler for a weak memory model.
My goal is to design a semantics for concurrent programming languages with
shared memory, such as Java, that allows many compiler optimisations while
giving reasonable guarantees to programmers. In my PhD thesis I describe how to
use trace-semantics to prove safety of common thread-local program transformations, such as
independent statement reordering and common subexpression elimination.
In my current research, I am trying to
extend the technique to prove safety of transformations that can introduce new memory accesses.
prove safety of transformations performed by processors using my thread-local transformations.
relate my trace semantic techniques to real compiler optimisations in a rigorous way (proof mechanisation).
explain global optimisations, include memory barriers...
Just like Peter, I believe that having a rigorous machine checked proof of
correctness of the memory model is necessary to have any confidence in the model.
Therefore, I am currently mechanizing the proofs in my dissertation in Isabelle/HOL.
HOL light proof replay
I have implemented a mechanism for replaying proofs in HOL light. This
significantly reduces the start-up time of HOL light (by about 50% on my machine), which is very useful if
checkpointing for some reason does not work for you.
The code can be downloaded here. Simply unpack to
the directory where you have installed HOL light, go to the Proofcache
directory and run the installcache script there. The script will
record the proofs during the HOL light startup, store them to a file, and
create a modified version of your hol.ml file that will use the stored
proofs instead of searching for proofs. Here is what you do to use the proof cache:
> cd ~/hol_light # or wherever your HOL light installation lives
> wget http://homepages.inf.ed.ac.uk/s0566973/proofcache.tgz
> tar -xzvf proofcache.tgz
> cd Proofcache
> ./installcache
.... wait ....
> cd ..
> ocaml
Objective Caml version 3.09.1
# #use "cachedhol.ml"
The cachedhol.ml version of HOL light should start about twice as fast
as the normal version of HOL light. If you want even faster startup, you can set
> export HOLPROOFCACHE=CHEAT
before starting ocaml. This will cause the proof cache to bypass the HOL kernel and create
all theorems in cache as axioms. This should buy you another 10-20% speedup.