Gopi: compiling linear and static channels in go

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

1 Citation (Scopus)
1 Downloads (Pure)

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.

Original languageEnglish
Title of host publicationCoordination Models and Languages - 22nd IFIP WG 6.1 International Conference, COORDINATION 2020, held as Part of the 15th International Federated Conference on Distributed Computing Techniques, DisCoTec 2020, Proceedings
EditorsSimon Bliudze, Laura Bocchi
Place of PublicationCham
PublisherSpringer
Pages137-152
Number of pages16
ISBN (Electronic)978-3-030-50029-0
ISBN (Print)978-3-030-50028-3
DOIs
Publication statusPublished - 2020
Event22nd IFIP WG 6.1 International Conference on Coordination Models and Languages, COORDINATION 2020, held as part of the 15th International Federated Conference on Distributed Computing Techniques, DisCoTec 2020 - Valletta, Malta
Duration: 15 Jun 202019 Jun 2020

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
PublisherSpringer
Volume12134 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference22nd IFIP WG 6.1 International Conference on Coordination Models and Languages, COORDINATION 2020, held as part of the 15th International Federated Conference on Distributed Computing Techniques, DisCoTec 2020
CountryMalta
CityValletta
Period15/06/2019/06/20

Fingerprint

Dive into the research topics of 'Gopi: compiling linear and static channels in go'. Together they form a unique fingerprint.

Cite this