Action Filename Description Size Access License Resource Version
Show more files...


Developing computer systems that are both concurrent and evolving is challenging. To guarantee consistent access to resources by concurrent software components, some synchronization is required. A synchronization logic, or policy, is at present entangled in the component code. Adding a new component or modifying existing components, which may require a change of the (global) synchronization policy, is therefore subjected to an extensive inspection of the complete code. We propose a calculus of concurrency combinators that allows a program code and its synchronization policy to be expressed separately; the policies include true parallelism, sequentiality, and isolation-only transactions. The calculus is equipped with an operational semantics and a type system. The type system is used to verify if a synchronization policy declared using combinators can be satisfied by program execution.