Captured: Compositional and Modular Approaches to Concurrency

In his paper “Wanted: A Compositional Approach to Concurrency” Cliff B. Jones convincingly claims that compositionality is a goal in software design. He describes why compositionality is a key property in software and systems engineering and why inherent interference make it difficult to find compositional specification and development methods for concurrent programs. In his paper, he identifies issues including action granularity and problems associated with ghost variables when dealing with assignment-oriented concurrent programs with shared variables. He also discusses atomicity as a design abstraction. In the following, we study compositional and, in the end, modular specification and verification approaches to concurrency for interactive systems based on data streams. Moreover, we define a concurrent assignment-oriented programming language and its translation into a formalism inspired by Leslie Lamport’s TLA. We discuss how far these approaches meet what is required by Cliff Jones in his article. Finally, we discuss the inherent difficulties in finding compositional and modular methods for concurrent software based on shared state.