Jaroslav Sevcik

Currently a researcher at the University of Edinburgh, School of Informatics (my CV)

Address

Room 8.12
Appleton Tower
11 Crichton Street
Edinburgh
EH8 9LE

Email: jarin.sevcik@gmail.com

Research interests

My research interests are programming languages, concurrency (Java Memory Model), semantics, and proof-carrying code. Currently I work on the ReQueST project and spend most of my time thinking about fixing and formalising the Java Memory Model.

Papers

Program Transformations in Weak Memory Models. PhD Thesis.
With David Aspinall: On Validity of Program Transformations in the Java Memory Model. ECOOP'08.
With David Aspinall: Formalising Java's Data Race Free Guarantee. TPHOLs 2007. Here is the Isabelle/HOL proof script.
With David Aspinall: Java Memory Model Examples: Good, Bad and Ugly. VAMP 2007 (a satellite workshop of CONCUR 2007).
Proving Resource Consumption of Low-level Programs Using Automated Theorem Provers. Bytecode 2007 (a satellite workshop at ETAPS 2007).

Projects

Weak memory models for high level languages

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, and lots of other things.

Proof mechanisation

The memory models are notoriously tricky to get right. For example, the Java Memory Model specification effort failed twice, even though the second attempt is a lot better (see my On Validity of Program Transformations in the Java Memory Model paper). The situation is probably not much better with processor memory models, see Peter Sewell's effort to formalise the Intel x86 memory model.

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 in Scala

Just for fun, I am porting the HOL light theorem prover to the JVM (using the Scala language) so that programmers can write tactics in any language that compiles to Java bytecode. My goals are:

Implement HOL kernel in Scala and replay all proofs from the HOL light distribution in the kernel.
Get rid of the global state in the prover (as opposed to HOL light).
Develop a Mizar-like language for tying proofs together using predefined tactics.
Use HOL light as proving backend, i.e., import proof objects from HOL light to the prover.
Most importantly, have fun!

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.

Teaching

Autumn 2005, 2006, 2007	Tutor for Algorithms and Data Structures (Edinburgh)
Spring 2005	Teaching assistant for Principles of Programming Languages (Rutgers)
Fall 2004	Teaching assistant for Numerical Analysis course (Rutgers)

My somewhat outdated research blog is here.