2017 - Technical Reports
Number Report Title 2017/1 Abstract Specifications for Concurrent Maps
Shale Xiong, Pedro da Rocha Pinto, Gian Ntzik and Philippa Gardner, 53pp
2017/2 A Linear Decomposition of Multiparty Sessions for Safe Distributed Programming
Alceste Scalas, Raymond Hu, Ornela Dardha and Nobuko Yoshido, 73pp
Shale Xiong, Pedro da Rocha Pinto, Gian Ntzik and Philippa Gardner, 53ppReport: 2017/1
Despite recent advances in reasoning about concurrent data structure libraries, the largest implementations in java.util.concurrent have yet to be verified. The key issue lies in the development of modular specifications, which provide clear logical boundaries between clients and implementations. A solution is to use recent advances in fine-grained concurrency reasoning, in particular the introduction of abstract atomicity to concurrent separation logic reasoning. We present two specifications of concurrent maps, both providing the clear boundaries we seek. We show that these specifications are equivalent, in that they can be built from each other. We show how we can verify client programs, such as a concurrent set and a producer-consumer client. We also give a substantial first proof that the main operations of ConcurrentSkipListMap in java.util.concurrent satisfy the map specification. This work demonstrates that we now have the technology to verify the largest implementations in java.util.concurrent.
Alceste Scalas, Raymond Hu, Ornela Dardha and Nobuko Yoshido, 73ppReport: 2017/2
Multiparty Session Types (MPST) is a typing discipline for message-passing distributed processes that can ensure properties such as absence of communication errors and deadlocks, and protocol conformance. Can MPST provide a theoretical foundation for concurrent and distributed programming in "mainstream" languages?
We address this problem by (1) developing the first encoding of a full-fledged multiparty session pi-calculus into standard linear pi-calculus, and (2) using the encoding as the foundation of a practical toolchain for safe multiparty programming in Scala.Our encoding is type-preserving and operationally sound and complete. Importantly for distributed applications, it preserves the choreographic nature of MPST and illuminates that multiparty sessions (and their safety properties) can be precisely represented with a decomposition into binary linear channels. Previous works have only studied the relation between (limited) multiparty sessions and binary sessions by orchestration means.
We exploit these results to implement an automated generation of Scala APIs for multiparty sessions. These APIs act as a layer on top of existing libraries for binary communication channels: this allows distributed multiparty systems to be safely implemented over binary transports, as commonly found in practice. Our implementation is also the first to support distributed multiparty delegation: our encoding yields it for free, via existing mechanisms for binary delegation.