by Graham on February 24, 2006.
Tagged as: Lunches.
Liyang and myself are currently trying to formally verify an implementation of a simplified version of the core language of STM Haskell, in order to have a precise understanding of the basic mechanisms for implementing transactions. We consider a small concurrent language that includes an atomicprimitive, and give this language an operational semantics. We then define a compiler for the language, which produces code for a virtual machine that implements the notion of transaction logs, and give this machine an operational semantics. The game then is the obvious one: establish a compiler correctness theorem that links the two semantics. In the meeting I gave a brief introduction to the notion of transactions, and posed an interesting problem: what is the appropriate notion of equality to be used when a transaction attempts to comit? We will say more about compiler correctness in the future, once this is finished.