31 pages, 3 figures. Submitted to ESOP 2021. This replaces a previous version with similar content, but has been heavily rewritten to reflect increased understanding of the contents
Common approaches to concurrent programming begin with languages whose semantics are naturally sequential and add new constructs that provide limited access to concurrency, as exemplified by futures. This approach has been quite successful, but often does not provide a satisfactory theoretical backing for the concurrency constructs, and it can be difficult to give a good semantics that allows a programmer to use more than one of these constructs at a time.
We take a different approach, starting with a concurrent language based on a Curry-Howard interpretation of adjoint logic, to which we add three atomic primitives that allow us to encode sequential composition and various forms of synchronization. The resulting language is highly expressive, allowing us to encode futures, fork/join parallelism, and monadic concurrency in the same framework. Notably, since our language is based on adjoint logic, we are able to give a formal account of linear futures, which have been used in complexity analysis by Blelloch and Reid-Miller. The uniformity of this approach means that we can similarly work with many of the other concurrency primitives in a linear fashion, and that we can mix several of these forms of concurrency in the same program to serve different purposes.
The increasingly concurrent and parallel landscape of hardware and software infrastructures demands the exploration and understanding of a wide variety of foundational and practical ideas. The International Workshop on Programming Language Approaches to Concurrency and Communication-cEntric Software (PLACES) is dedicated to work in this area. The workshop offers a forum for researchers from different fields to exchange new ideas about these challenges to modern and future programming, where concurrency and distribution are the norm rather than a marginal concern. The topic is central and combi…
Go is an increasingly-popular systems programming language targeting, especially, concurrent and distributed systems. Go differentiates itself from other imperative languages by offering structural subtyping and lightweight concurrency through goroutines with message-passing communication. This combination of features poses interesting challenges for static verification, most prominently the combination of a mutable heap and advanced concurrency primitives. We present Gobra, a modular, deductive program verifier for Go that proves memory safety, crash safety, data-race freedom, and user-provid…
