Skip to Main content Skip to Navigation
Conference papers

GoPi: Compiling Linear and Static Channels in Go

Abstract : We identify two important features to enhance the design of communication protocols specified in the pi-calculus, that are linear and static channels, and present a compiler, named GoPi, that maps high level specifications into executable Go programs. Channels declared as linear are deadlock-free, while the scope of static channels, which are bound by a hide declaration, does not enlarge at runtime; this is enforced statically by means of type inference, while specifications do not include annotations. Well-behaved processes are transformed into Go code that supports non-deterministic synchronizations and race-freedom. We sketch two main examples involving protection against message forwarding, and forward secrecy, and discuss the features of the tool, and the generated code. We argue that GoPi can support academic activities involving process algebras and formal models, which range from the analysis and testing of concurrent processes for research purposes to teaching formal languages and concurrent systems.
Complete list of metadata

https://hal.inria.fr/hal-03273983
Contributor : Hal Ifip Connect in order to contact the contributor
Submitted on : Tuesday, June 29, 2021 - 4:12:39 PM
Last modification on : Tuesday, June 29, 2021 - 4:30:49 PM
Long-term archiving on: : Thursday, September 30, 2021 - 7:12:35 PM

File

 Restricted access
To satisfy the distribution rights of the publisher, the document is embargoed until : 2023-01-01

Please log in to resquest access to the document

Licence


Distributed under a Creative Commons Attribution 4.0 International License

Identifiers

Citation

Marco Giunti. GoPi: Compiling Linear and Static Channels in Go. 22th International Conference on Coordination Languages and Models (COORDINATION), Jun 2020, Valletta, Malta. pp.137-152, ⟨10.1007/978-3-030-50029-0_9⟩. ⟨hal-03273983⟩

Share

Metrics

Record views

13