CMU-ISR-08-126
Institute for Software Research
School of Computer Science, Carnegie Mellon University



CMU-ISR-08-126

Verifying Correct Usage of Atomic Blocks
and Typestate: Technical Companion

Nels E. Beckman, Jonathan Aldrich

August 2008

CMU-ISR-08-126.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 well-typed expressions evaluate to other well-typed expressions, and a proof of progress, which shows that well-typed 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 well-typed heap, which ensures that only one reference in the entire thread-pool can know the exact state of an object of share or pure permission.

43 pages


Return to: SCS Technical Report Collection
School of Computer Science homepage

This page maintained by reports@cs.cmu.edu