
arXiv: 1710.03928
AbstractA number of high-level languages and libraries have been proposed that offer novel and simple to use abstractions for concurrent, asynchronous, and distributed programming. The execution models that realise them, however, often change over time—whether to improve performance, or to extend them to new language features—potentially affecting behavioural and safety properties of existing programs. This is exemplified byScoop, a message-passing approach to concurrent object-oriented programming that has seen multiple changes proposed and implemented, with demonstrable consequences for an idiomatic usage of its core abstraction. We propose asemantics comparison workbenchforScoopwith fully and semi-automatic tools for analysing and comparing the state spaces of programs with respect to different execution models or semantics. We demonstrate its use in checking the consistency of properties across semantics by applying it to a set of representative programs, and highlighting a deadlock-related discrepancy between the principal execution models ofScoop. Furthermore, we demonstrate the extensibility of the workbench by generalising the formalisation of an execution model to support recently proposed extensions for distributed programming. Our workbench is based on a modular and parameterisable graph transformation semantics implemented in theGroovetool. We discuss how graph transformations are leveraged to atomically model intricate language abstractions, how the visual yet algebraic nature of the model can be used to ascertain soundness, and highlight how the approach could be applied to similar languages.
FOS: Computer and information sciences, Computer Science - Logic in Computer Science, runtime semantics, Computer Science - Software Engineering, Computer Science - Programming Languages, verification/analysis parameterised by semantics, object-oriented programming, SCOOP, GROOVE, concurrency abstractions, Logic in Computer Science (cs.LO), Software Engineering (cs.SE), Programming Languages and Compilers, Computer Science - Distributed, Parallel, and Cluster Computing, distributed programming with message passing, operational semantics, concurrent asynchronous programming, graph transformation systems, Distributed, Parallel, and Cluster Computing (cs.DC), software engineering, Programming Languages (cs.PL)
FOS: Computer and information sciences, Computer Science - Logic in Computer Science, runtime semantics, Computer Science - Software Engineering, Computer Science - Programming Languages, verification/analysis parameterised by semantics, object-oriented programming, SCOOP, GROOVE, concurrency abstractions, Logic in Computer Science (cs.LO), Software Engineering (cs.SE), Programming Languages and Compilers, Computer Science - Distributed, Parallel, and Cluster Computing, distributed programming with message passing, operational semantics, concurrent asynchronous programming, graph transformation systems, Distributed, Parallel, and Cluster Computing (cs.DC), software engineering, Programming Languages (cs.PL)
| selected citations These citations are derived from selected sources. This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | 2 | |
| popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network. | Average | |
| influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | Average | |
| impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network. | Average |
