arXiv subjects

Ian J. Hayes

Publications and source records attributed to Ian J. Hayes.

24 records · Page 2Linked to original sources

arXiv2017

A synchronous program algebra: a basis for reasoning about shared-memory and event-based concurrency

This research started with an algebra for reasoning about rely/guarantee concurrency for a shared memory model. The approach taken led to a more abstract algebra of atomic steps, in which atomic steps synchronise (rather than interleave) when composed in parallel. The algebra of rely/guarantee concurrency then becomes an instantiation of the more abstract algebra. Many of the core properties needed for rely/guarantee reasoning can be shown to hold in the abstract algebra where their proofs are simpler and hence allow a higher degree of automation. The algebra has been encoded in Isabelle/HOL to provide a basis for tool support for program verification. In rely/guarantee concurrency, programs are specified to guarantee certain behaviours until assumptions about the behaviour of their environment are violated. When assumptions are violated, program behaviour is unconstrained (aborting), and guarantees need no longer hold. To support these guarantees a second synchronous operator, weak conjunction, was introduced: both processes in a weak conjunction must agree to take each atomic step, unless one aborts in which case the whole aborts. In developing the laws for parallel and weak conjunction we found many properties were shared by the operators and that the proofs of many laws were essentially the same. This insight led to the idea of generalising synchronisation to an abstract operator with only the axioms that are shared by the parallel and weak conjunction operator, so that those two operators can be viewed as instantiations of the abstract synchronisation operator. The main differences between parallel and weak conjunction are how they combine individual atomic steps; that is left open in the axioms for the abstract operator.

cs.LO↗

arXiv2016

Designing a semantic model for a wide-spectrum language with concurrency

A wide-spectrum language integrates specification constructs into a programming language in a manner that treats a specification command just like any other command. This paper investigates a semantic model for a wide-spectrum language that supports concurrency and a refinement calculus. In order to handle specifications with rely and guarantee conditions, the model includes explicit environment steps as well as program steps. A novelty of our approach is that we define a set of primitive commands and operators, from which more complex specification and programming language commands are built. The primitives have simple algebraic properties which support proof using algebraic reasoning. The model is general enough to specify notions as diverse as rely-guarantee reasoning, temporal logic, and progress properties of programs, and supports refining specifications to code. It also forms an instance of an abstract concurrent program algebra, which facilitates reasoning about properties of the model at a high level of abstraction.

cs.LO↗

arXiv2016

Generalised rely-guarantee concurrency: An algebraic foundation

The rely-guarantee technique allows one to reason compositionally about concurrent programs. To handle interference the technique makes use of rely and guarantee conditions, both of which are binary relations on states. A rely condition is an assumption that the environment performs only atomic steps satisfying the rely relation and a guarantee is a commitment that every atomic step the program makes satisfies the guarantee relation. In order to investigate rely-guarantee reasoning more generally, in this paper we allow interference to be represented by a process rather than a relation and hence derive more general rely-guarantee laws. The paper makes use of a weak conjunction operator between processes, which generalises a guarantee relation to a guarantee process, and introduces a rely quotient operator, which generalises a rely relation to a process. The paper focuses on the algebraic properties of the general rely-guarantee theory. The Jones-style rely-guarantee theory can be interpreted as a model of the general algebraic theory and hence the general laws presented here hold for that theory.

cs.LO↗

arXiv2016

Possible values: exploring a concept for concurrency

An important issue in concurrency is interference. This issue manifests itself in both shared-variable and communication-based concurrency --- this paper focusses on the former case where interference is caused by the environment of a process changing the values of shared variables. Rely/guarantee approaches have been shown to be useful in specifying and reasoning compositionally about concurrent programs. This paper explores the use of a "possible values" notation for reasoning about variables whose values can be changed multiple times by interference. Apart from the value of this concept in providing clear specifications, it offers a principled way of avoiding the need for some auxiliary (or ghost) variables whose unwise use can destroy compositionality.

cs.LO↗

arXiv2014

Convolution, Separation and Concurrency

A notion of convolution is presented in the context of formal power series together with lifting constructions characterising algebras of such series, which usually are quantales. A number of examples underpin the universality of these constructions, the most prominent ones being separation logics, where convolution is separating conjunction in an assertion quantale; interval logics, where convolution is the chop operation; and stream interval functions, where convolution is used for analysing the trajectories of dynamical or real-time systems. A Hoare logic is constructed in a generic fashion on the power series quantale, which applies to each of these examples. In many cases, commutative notions of convolution have natural interpretations as concurrency operations.

cs.LO↗

arXiv2006

Calculating modules in contextual logic program refinement

The refinement calculus for logic programs is a framework for deriving logic programs from specifications. It is based on a wide-spectrum language that can express both specifications and code, and a refinement relation that models the notion of correct implementation. In this paper we extend and generalise earlier work on contextual refinement. Contextual refinement simplifies the refinement process by abstractly capturing the context of a subcomponent of a program, which typically includes information about the values of the free variables. This paper also extends and generalises module refinement. A module is a collection of procedures that operate on a common data type; module refinement between a specification module A and an implementation module C allows calls to the procedures of A to be systematically replaced with calls to the corresponding procedures of C. Based on the conditions for module refinement, we present a method for calculating an implementation module from a specification module. Both contextual and module refinement within the refinement calculus have been generalised from earlier work and the results are presented in a unified framework.

cs.LO↗