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

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.