Toggle Main Menu Toggle Search

Open Access padlockePrints

[PhD Thesis] Constructing a Tractable Reasoning Framework upon a Fine-Grained Structural Operational Semantics

Lookup NU author(s): Dr Joey Coleman

Downloads

Full text is not currently available for this publication.


Abstract

The primary focus of this thesis is the semantic gap between a fine-grained structural operational semantics and a set of rely/guarantee-style development rules. The semantic gap is bridged by considering the development rules to be a part of the same logical framework as the operational semantics, and a set of soundness proofs show that the development rules, though making development easier for a developer, do not add any extra power to the logical framework as a whole. The soundness proofs given are constructed to take advantage of the structural nature of the language and its semantics; this allows for the addition of new development rules in a modular fashion. The particular language semantics allows for very fine-grained concurrency. The language itself includes a construct for nested parallel execution of statements, and the semantics is written so that statements can interfere with each other between individual variable reads. The language also includes an atomic block construct for which the semantics is an embodiment of a form of software transactional memory. The inclusion of the atomic construct helps illustrate the inherent expressive weakness present in the rely/guarantee rules with respect to termination properties. As such, two development rules are proposed for the atomic construct, one of which has serious restrictions in its application, and another for which the termination property does not hold.


Publication metadata

Author(s): Coleman JW

Publication type: Report

Publication status: Published

Series Title:

Year: 2008

Institution: School of Computing Science, University of Newcastle upon Tyne

Place Published: Newcastle upon Tyne


Share