Relation-based semantics for concurrency (Q1328556): Difference between revisions

``Despite several decades of research, capturing the semantics of concurrent programs in a crisp and tractable fashion remains a formidable challenge''. With this ambitious goal the authors initiate their quest towards the clean and manageable concurrency semantics many have searched for before with more or less success. To bad for the present authors that they can't be recognized to be among the small group of survivors who actually made it. The treatment is based on a relational model in a state space consisting of global states being the Cartesian product of domains for individual (possibly shared) variables and/or shared Booleans. Each component process involves a Cartesian factor of this state space. Atomic fragments of the program are mapped on relations on these component spaces (lifted towards the full state space). Sequential composition is obtained by relation product. The difficult construct is the parallel composition which here is represented by an infinitary operator which actually represents the union of all intersections of semi-synchronized interleavings. As an application the authors indicate how to invoke their semantics for the detection of potential deadlocks. The aims as claimed by the authors consists of reaching three properties for their semantics: Compositionality, Axiomatics, and Modularity. As stated informally in the introduction it is difficult to understand the difference between Compositionality and Modularity, since both notions require that the meaning of a complex entity is obtained by combining the meanings of their constituent parts; what is hidden behind this distinction is that compositionality refers to the individual processes and modularity to the parallel operator\dots Also the notion of axiomatics is non standard: the authors don't introduce a logical language describing sets of states as propositions or predicates, providing for an axiomatic characterization of the various operators, but just refer to the fact that the semantics is described in terms of logical formulas in a mathematical meta-language. My main objection is however that the parallel operator as proposed is not compositional at all. The operator considers processes to be obtained as the parallel combination of sequences of atomic processes, in order that the full range of all possible interleavings can be obtained. But then the sequential composition of these atomic parts within a component process is never build as a syntactic entity, hiding its internal structure for the semantic parallel operator. Moreover, there doesn't exist a single parallel operator but an entire infinitary family of such operators. Which contravenes the targets set by the authors. Overall I feel that the appreciation of the state of the art by the authors is overall pessimistic. The literature by now has shown in a convincing way that the parallel composition is adequately modelled by an intersection operator working on the semantics of the component programs provided these component semantics are enriched sufficiently to represent the fact that a component is assumed to operate within an environment which is unknown at the time the component semantics is determined. From a sufficiently abstract perspective this is what the present authors are doing as well, be it in a rather unconvincing way.