Verifying Correct Usage of Atomic Blocks and Typestate: Technical Companion

Abstract

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.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Aug 01, 2008
Accession Number
ADA488523

Entities

People

  • Jonathan Erik Aldrich
  • Nels E. Beckman

Organizations

  • Carnegie Mellon University

Tags

DTIC Thesaurus Topics

  • Computer Science
  • Computers
  • Department Of Defense
  • Formal Languages
  • Information Operations
  • Inversion
  • Judgment
  • Language
  • Military Research
  • Schools
  • Semantics
  • Test And Evaluation
  • Universities
  • Words (Language)

Fields of Study

  • Computer science

Readers

  • Computational Linguistics
  • Parallel and Distributed Computing.