Truly Concurrent Models of Programs with Resources

Abstract

The graph-based semantics introduced in the previous chapter is often not informative enough, because it does not take into account whether two actions commute or not. In this chapter, we introduce truly concurrent models which incorporate this information. We begin by extending our programming languages with resources and restrict ourselves to conservative programs, in which resource consumption only depends on the current state. We then generalize the semantics to asynchronous graphs, which explicitly describe the commutation of two actions and to precubical sets, which can more generally express the commutation of n actions. Finally, links with other classical models for concurrency are mentioned.