WoTUG - The place for concurrent processes

Papers that include Dr. Adrian E. Lawrence as an Author

Name: Dr. Adrian E. Lawrence
Papers:

Title: Extending CSP
Authors: Adrian E. Lawrence
Abstract:

CSP, timed or untimed, has not included a general treatment of priority, although the PRI ALT constructor is an essential part of occam. This paper introduces CSPP which includes a generalization of PRI ALT in the form of a prioritized external choice P <pribox> Q. PRI PAR is also included. A new denotational semantics is introduced, although only the simplest model is outlined. The work is intended to provide a solid rogorous foundation for hardware-software codesign. And a companion paper describes untimed HCSP which is a further extension of CSP built upon these foundations. It was first presented informally at the Twente WoTUG-20 technical meeting.

Bibliography: Web page:BibTEX, Refer
Plain text: BibTEX, Refer
In Proceeding:

Proceedings of WoTUG-21: Architectures, Languages and Patterns for Parallel and Distributed Applications,


Title: HCSP: Extending CSP for Codesign and Shared Memory
Authors: Adrian E. Lawrence
Abstract:

HCSP is a variant of CSP adapted to capture the semantics of hardware compilation, among other purposes. It extends CSP in several ways; it includes priority; events can be combined; new synchronization constructors are introduced; and state is explicitly modelled. Including state permits the treatment of shared memory as well as message passing systems. A possible denotational semantics is included here ths allowing proper treatment of such systems. Although most of these extensions were motivated by the needs of hardware compilation, HCSP can be applied more widely including software and thus can form the foundation of a codesign language. HCSP is an extension of CSPP; familiarity of CSPP is assumed here.

Bibliography: Web page:BibTEX, Refer
Plain text: BibTEX, Refer
In Proceeding:

Proceedings of WoTUG-21: Architectures, Languages and Patterns for Parallel and Distributed Applications,


Title: Hard and Soft Priority in CSP
Authors: Adrian E. Lawrence
Abstract: Parallel systems which include priority can experience conflicts when two concurrent processes assign different priorities to the same actions. There are at least two ways to resolve the difficulty: one is to halt; the other is to declare a draw and allocate all the offending actions the same priority. In CSPP these are called respectively hard and soft priority. Originally CSPP included only hard priority. Here we extend the language to include soft priority as well. The Acceptances semantics which is used to define CSPP does not require modification: it captures both soft and hard behaviours.
Bibliography: Web page:BibTEX, Refer
Plain text: BibTEX, Refer
In Proceeding:

Proceedings of WoTUG-22: Architectures, Languages and Techniques for Concurrent Systems,


Title: Successes and Failures: Extending CSP
Authors: Adrian E. Lawrence
Abstract:

Standard CSP, timed or untimed, does not include a general treatment of priority, although the PRI ALT constructor is an essential part of occam and hardware compilation languages based upon occam. This is a revised version of the original paper which introduced CSPP, an extension of CSP incorporating priority. CSPP is defined by a novel denotational semantics, Acceptances, based on Successes rather than the usual Failures. The idea is to characterise a process by what it successfully accepts, rather than by what it refuses to do. In the light of experience, it might better have been called 'Responses'. The original Acceptances was exploratory, and tried to avoid constraining the sorts of systems, particularly circuits, that could be described. Experience has shown that it can be substantially simplified at very little cost. A new notation makes it much easier to follow, especially for the non specialist. This revision of the original introduction presents the simplified CSPP while retaining most of the motivational material. It is intended to have something of a tutorial flavour: three other papers, are more condensed, and deal with more technical matters. But the core semantics is common to all four. CSPP provides a rigorous comprehensible and simple foundation for compositional hardware-software codesign. HCSP is a further extension which includes extra facilities needed to describe certain circuits. And a further radical extension lifts the usual restrictions of timed CSP, and describes continuous analogue phenomena. CSPP was first presented informally at the Twente WoTUG--20 technical meeting.

Bibliography: Web page:BibTEX, Refer
Plain text: BibTEX, Refer
In Proceeding:

Communicating Process Architectures 2001,


Title: CSPP and Event Priority
Authors: Adrian E. Lawrence
Abstract:

CSPP is an extension of CSP which includes priority as used in standard occam. The occam community has often discussed whether those notions are really adequate, a particular concern being the difficulties associated with priority inversion. One idea is to give priority to sets of events considered independently of the processes that perform them. We call this 'event priority'. Event priority is static in this presentation. But it is possible to handle dynamic priority using a global synchronisation when the 'event priority' changes. Obviously there is no problem for a software system with a central scheduler, but the theory here is addressing a far wider class of systems, in particular massively parallel, widely distributed, implemented in either hardware or software or both. It may be that some higher level of abstraction should replace priority: priority is a mechanism for achieving certain properties, often relating to time and limited resources. Here we content ourselves with finding a formal description of a language including event-priority.

Bibliography: Web page:BibTEX, Refer
Plain text: BibTEX, Refer
In Proceeding:

Communicating Process Architectures 2001,


Title: Infinite Traces, Acceptances and CSPP
Authors: Adrian E. Lawrence
Abstract:

There is a long standing problem when infinite traces are included in denotational semantic models of CSP. Full models fail to be Complete Partial Orders under refinement. This paper introduces a novel, but entirely natural, way of representing infinite behaviour in which refinement is a Complete Partial Order when the alphabet of events is finite. Acceptance semantics also solves the problem of infinite behaviour with an infinite alphabet. That requires a different construction based on a metric space and will be described elsewhere.

Bibliography: Web page:BibTEX, Refer
Plain text: BibTEX, Refer
In Proceeding:

Communicating Process Architectures 2001,


Title: Acceptances, Behaviours and Infinite Activity in CSPP
Authors: Adrian E. Lawrence
Abstract:

The denotational semantics presented here defines an extension of CSP called CSPP. It includes a full description of infinite behaviour in one simple model using only finite traces. This is true for both finite and infinite alphabets. The structure is a complete lattice, and so also a complete partial order, under refinement. Thus recursion is defined by fixed points in the usual way. It is also a complete restriction metric space so this provides an alternative treatment of recursion for contraction mappings.

Bibliography: Web page:BibTEX, Refer
Plain text: BibTEX, Refer
In Proceeding:

Communicating Process Architectures 2002,

Files:PS, PDF

Title: HCSP: Imperative State and True Concurrency
Authors: Adrian E. Lawrence
Abstract:

HCSP is an extension of CSPP which captures the semantics of hardware compilation. Because it is a superset of CSPP, it can describe both hardware and software and so is useful for co-design. The extensions beyond CSPP include: true concurrency; new hardware constructors; and a simple and natural way to represent imperative state. Both CSPP and HCSP were invented to cope with problems that arose while the author was trying to prove that the hardware that he had designed correctly implemented channels between a processor and an FPGA. Standard CSP did not capture priority, yet the circuits in the FPGA and the occam processes in the transputer both depended on priority for their correctness. The attempt to extend CSP rigorously to handle such problems of co-design has led to develoments that seem to have a much wider significance including a new way of unifying theories for imperative programming. This paper reports on the current state of HCSP and focuses on handling imperative state and true concurrency. The acceptance denotational semantics is described briefly.

Bibliography: Web page:BibTEX, Refer
Plain text: BibTEX, Refer
In Proceeding:

Communicating Process Architectures 2002,

Files:PS, PDF

Title: Overtures and hesitant offers: hiding in CSPP
Authors: Adrian E. Lawrence
Abstract:

Hiding is an important and characteristic part of CSP. Defining it in thepresence of priority for CSPP needs care. The ideas of overtures and hesitant offersintroduced here arise naturally in the context of Acceptances. They provide clearinsight into the behaviour of hidden processes. And particularly illuminate the originof the nondeterminism which frequently arises from hiding.Keywords: CSP; CSPP; Denotational semantics; formal methods; concurrency; parallelsystems; occam; hardware compilation; priority; hiding.

Bibliography: Web page:BibTEX, Refer
Plain text: BibTEX, Refer
In Proceeding:

Communicating Process Architectures 2003,

Files:PDF

Title: Observing Processes
Authors: Adrian E. Lawrence
Abstract:

This paper discusses the sorts of observations of processes that are appropriate to capture priority. The standard denotational semantics for CSP are based around observations of traces and refusals. Choosing to record a little more detail allows extensions of CSP which describe some very general processes including those that include priority. A minimal set of observations yields a language and semantics remarkably close to the standard Failures-Divergences model of CSP which is described in a companion paper. A slightly richer set of observations yields a somewhat less abstract language.

Bibliography: Web page:BibTEX, Refer
Plain text: BibTEX, Refer
In Proceeding:

Communicating Process Architectures 2004,

Files:PDF

Title: Triples
Authors: Adrian E. Lawrence
Abstract:

The most abstract form of acceptance semantics for a variant of CSPP is outlined. It encompasses processes which may involve priority, but covers a much wider class of systems including real time behaviour. It shares many of the features of the standard Failures-Divergences treatment: thus it is only a Complete Partial Order when the alphabet of events is finite.

Bibliography: Web page:BibTEX, Refer
Plain text: BibTEX, Refer
In Proceeding:

Communicating Process Architectures 2004,

Files:PDF

If you have any comments on this database, including inaccuracies, requests to remove or add information, or suggestions for improvement, the WoTUG web team are happy to hear of them. We will do our best to resolve problems to everyone's satisfaction.

Copyright for the papers presented in this database normally resides with the authors; please contact them directly for more information. Addresses are normally presented in the full paper.

Pages © WoTUG, or the indicated author. All Rights Reserved.
Comments on these web pages should be addressed to: www at wotug.org

Valid HTML 4.01!