
CMUISR08126
Institute for Software Research
School of Computer Science, Carnegie Mellon University
CMUISR08126
Verifying Correct Usage of Atomic Blocks
and Typestate: Technical Companion
Nels E. Beckman, Jonathan Aldrich
August 2008
CMUISR08126.pdf
Keywords: Transactional memory, typestate, proof
In this technical report, we present a static and dynamic semantics as well
as a proof of soundness for a programming language presented in the paper
entitled, Verifying Correct Usage of Atomic Blocks and Typestate. The
proof of soundness consists of a proof of preservation, which shows
that welltyped expressions evaluate to other welltyped expressions, and
a proof of progress, which shows that welltyped expressions are either
values or can take an evaluation step in the dynamic semantics. The notion
of progress is complicated by a specific notion of a welltyped
heap, which ensures that only one reference in the entire threadpool can
know the exact state of an object of share or pure permission.
43 pages
