Showing 1–27 of 27 results for author: Vasconcelos, V T

Behavioural Types for Heterogeneous Systems (Position Paper)

Authors: Simon Fowler, Philipp Haller, Roland Kuhn, Sam Lindley, Alceste Scalas, Vasco T. Vasconcelos

Abstract: Behavioural types provide a promising way to achieve lightweight, language-integrated verification for communication-centric software. However, a large barrier to the adoption of behavioural types is that the current state of the art expects software to be written using the same tools and ty** discipline throughout a system, and has little support for components over which a developer has no con… ▽ More Behavioural types provide a promising way to achieve lightweight, language-integrated verification for communication-centric software. However, a large barrier to the adoption of behavioural types is that the current state of the art expects software to be written using the same tools and ty** discipline throughout a system, and has little support for components over which a developer has no control. This position paper describes the outcomes of a working group discussion at Dagstuhl Seminar 24051 (Next-Generation Protocols for Heterogeneous Systems). We propose a methodology for integrating multiple behaviourally-typed components, written in different languages. Our proposed approach involves an extensible protocol description language, a session IR that can describe data transformations and boundary monitoring and which can be compiled into program-specific session proxies, and finally a session middleware to aid session establishment. We hope that this position paper will stimulate discussion on one of the most pressing challenges facing the widespread adoption of behavioural ty**. △ Less

Submitted 8 April, 2024; originally announced April 2024.

Comments: In Proceedings PLACES 2024, arXiv:2404.03712

Journal ref: EPTCS 401, 2024, pp. 37-48

Linear Contextual Metaprogramming and Session Types

Authors: Pedro Ângelo, Atsushi Igarashi, Vasco T. Vasconcelos

Abstract: We explore the integration of metaprogramming in a call-by-value linear lambda-calculus and sketch its extension to a session type system. We build on a model of contextual modal type theory with multi-level contexts, where contextual values, closing arbitrary terms over a series of variables, may then be boxed and transmitted in messages. Once received, one such value may then be unboxed (with a… ▽ More We explore the integration of metaprogramming in a call-by-value linear lambda-calculus and sketch its extension to a session type system. We build on a model of contextual modal type theory with multi-level contexts, where contextual values, closing arbitrary terms over a series of variables, may then be boxed and transmitted in messages. Once received, one such value may then be unboxed (with a let-box construct) and locally applied before being run. We present a series of examples where servers prepare and ship code on demand via session typed messages. △ Less

Submitted 8 April, 2024; originally announced April 2024.

Comments: In Proceedings PLACES 2024, arXiv:2404.03712

Journal ref: EPTCS 401, 2024, pp. 1-10

Subty** Context-Free Session Types

Authors: Gil Silva, Andreia Mordido, Vasco T. Vasconcelos

Abstract: Context-free session types describe structured patterns of communication on heterogeneously-typed channels, allowing the specification of protocols unconstrained by tail recursion. The enhanced expressive power provided by non-regular recursion comes, however, at the cost of the decidability of subty**, even if equivalence is still decidable. We present an approach to subty** context-free sess… ▽ More Context-free session types describe structured patterns of communication on heterogeneously-typed channels, allowing the specification of protocols unconstrained by tail recursion. The enhanced expressive power provided by non-regular recursion comes, however, at the cost of the decidability of subty**, even if equivalence is still decidable. We present an approach to subty** context-free session types based on a novel kind of observational preorder we call $\mathcal{XYZW}$-simulation, which generalizes $\mathcal{XY}$-simulation (also known as covariant-contravariant simulation) and therefore also bisimulation and plain simulation. We further propose a subty** algorithm that we prove to be sound, and present an empirical evaluation in the context of a compiler for a programming language. Due to the general nature of the simulation relation upon which it is built, this algorithm may also find applications in other domains. △ Less

Submitted 20 September, 2023; v1 submitted 11 July, 2023; originally announced July 2023.

Comments: 34 pages, 6 figures, technical report of a paper published in the conference proceedings of CONCUR 2023

Journal ref: Leibniz International Proceedings in Informatics (LIPIcs), 34th International Conference on Concurrency Theory (CONCUR 2023), pp.11:1-11:19

Kind Inference for the FreeST Programming Language

Authors: Bernardo Almeida, Andreia Mordido, Vasco T. Vasconcelos

Abstract: We present a kind inference algorithm for the FREEST programming language. The input to the algorithm is FREEST source code with (possibly part of) kind annotations replaced by kind variables. The algorithm infers concrete kinds for all kind variables. We ran the algorithm on the FREEST test suite by first replacing kind annotation on all type variables by fresh kind variables, and concluded that… ▽ More We present a kind inference algorithm for the FREEST programming language. The input to the algorithm is FREEST source code with (possibly part of) kind annotations replaced by kind variables. The algorithm infers concrete kinds for all kind variables. We ran the algorithm on the FREEST test suite by first replacing kind annotation on all type variables by fresh kind variables, and concluded that the algorithm correctly infers all kinds. Non surprisingly, we found out that programmers do not choose the most general kind in 20% of the cases. △ Less

Submitted 13 April, 2023; originally announced April 2023.

Comments: In Proceedings PLACES 2023, arXiv:2304.05439

Journal ref: EPTCS 378, 2023, pp. 1-13

Parameterized Algebraic Protocols

Authors: Andreia Mordido, Janek Spaderna, Peter Thiemann, Vasco T. Vasconcelos

Abstract: We propose algebraic protocols that enable the definition of protocol templates and session types analogous to the definition of domain-specific types with algebraic datatypes. Parameterized algebraic protocols subsume all regular as well as most context-free and nested session types and, at the same time, replace the expensive superlinear algorithms for type checking by a nominal check that runs… ▽ More We propose algebraic protocols that enable the definition of protocol templates and session types analogous to the definition of domain-specific types with algebraic datatypes. Parameterized algebraic protocols subsume all regular as well as most context-free and nested session types and, at the same time, replace the expensive superlinear algorithms for type checking by a nominal check that runs in linear time. Algebraic protocols in combination with polymorphism increase expressiveness and modularity by facilitating new ways of parameterizing and composing session types. △ Less

Submitted 7 April, 2023; originally announced April 2023.

ACM Class: D.3.1

System $F^μ_ω$ with Context-free Session Types

Authors: Diana Costa, Andreia Mordido, Diogo Poças, Vasco T. Vasconcelos

Abstract: We study increasingly expressive type systems, from $F^μ$ -- an extension of the polymorphic lambda calculus with equirecursive types -- to $F^{μ;}_ω$ -- the higher-order polymorphic lambda calculus with equirecursive types and context-free session types. Type equivalence is given by a standard bisimulation defined over a novel labelled transition system for types. Our system subsumes the contract… ▽ More We study increasingly expressive type systems, from $F^μ$ -- an extension of the polymorphic lambda calculus with equirecursive types -- to $F^{μ;}_ω$ -- the higher-order polymorphic lambda calculus with equirecursive types and context-free session types. Type equivalence is given by a standard bisimulation defined over a novel labelled transition system for types. Our system subsumes the contractive fragment of $F^μ_ω$ as studied in the literature. Decidability results for type equivalence of the various type languages are obtained from the translation of types into objects of an appropriate computational model: finite-state automata, simple grammars and deterministic pushdown automata. We show that type equivalence is decidable for a significant fragment of the type language. We further propose a message-passing, concurrent functional language equipped with the expressive type language and show that it enjoys preservation and absence of runtime errors for typable processes. △ Less

Submitted 20 January, 2023; originally announced January 2023.

Comments: 38 pages, 13 figures

Higher-order Context-free Session Types in System F

Authors: Diana Costa, Andreia Mordido, Diogo Poças, Vasco T. Vasconcelos

Abstract: We present an extension of System F with higher-order context-free session types. The mixture of functional types with session types has proven to be a challenge for type equivalence formalization: whereas functional type equivalence is often rule-based, session type equivalence usually follows a semantic approach based on bisimulations. We propose a unifying approach that handles the equivalence… ▽ More We present an extension of System F with higher-order context-free session types. The mixture of functional types with session types has proven to be a challenge for type equivalence formalization: whereas functional type equivalence is often rule-based, session type equivalence usually follows a semantic approach based on bisimulations. We propose a unifying approach that handles the equivalence of functional and session types together. We present three notions of type equivalence: a syntactic rule-based version, a semantic bisimulation-based version, and an algorithmic version by reduction to the problem of bisimulation of simple grammars. We prove that the three notions coincide and derive a decidability result for the type equivalence problem of higher-order context-free session types. △ Less

Submitted 24 March, 2022; originally announced March 2022.

Comments: In Proceedings PLACES 2022, arXiv:2203.12142

Journal ref: EPTCS 356, 2022, pp. 24-35

The Different Shades of Infinite Session Types

Authors: Simon J. Gay, Diogo Poças, Vasco T. Vasconcelos

Abstract: Many type systems include infinite types. In session type systems, which are the focus of this paper, infinite types are important because they allow the specification of communication protocols that are unbounded in time. Usually infinite session types are introduced as simple finite-state expressions $\mathsf{rec}\, X.T$ or by non-parametric equational definitions $X\doteq T$. Alternatively, som… ▽ More Many type systems include infinite types. In session type systems, which are the focus of this paper, infinite types are important because they allow the specification of communication protocols that are unbounded in time. Usually infinite session types are introduced as simple finite-state expressions $\mathsf{rec}\, X.T$ or by non-parametric equational definitions $X\doteq T$. Alternatively, some systems of label- or value-dependent session types go beyond simple recursive types. However, leaving dependent types aside, there is a much richer world of infinite session types, ranging through various forms of parametric equational definitions, all the way to arbitrary infinite types in a coinductively defined space. We study infinite session types across a spectrum of shades of grey on the way to the bright light of general infinite types. We identify four points on the spectrum, characterised by different styles of equational definitions, and show that they form a strict hierarchy by establishing bidirectional correspondences with classes of automata: finite-state, 1-counter, pushdown and 2-counter. This allows us to establish decidability and undecidability results for the problems of type formation, type equivalence and duality in each class of types. We also consider previous work on context-free session types (and extend it to higher-order) and nested session types, and locate them on our spectrum of infinite types. △ Less

Submitted 20 January, 2022; originally announced January 2022.

Comments: 51 pages, 12 figures

Protocol-based Smart Contract Generation

Authors: Afonso Falcão, Andreia Mordido, Vasco T. Vasconcelos

Abstract: The popularity of smart contracts is on the rise, yet breaches in reliability and security linger. Among the many facets of smart contract reliability, we concentrate on faults rooted in out-of-order interactions with contract endpoints. We propose SmartScribble, a protocol language to describe valid patterns of interaction between users and endpoints. SmartScribble not only ensures correct intera… ▽ More The popularity of smart contracts is on the rise, yet breaches in reliability and security linger. Among the many facets of smart contract reliability, we concentrate on faults rooted in out-of-order interactions with contract endpoints. We propose SmartScribble, a protocol language to describe valid patterns of interaction between users and endpoints. SmartScribble not only ensures correct interactive behaviour but also simplifies smart contract coding. From a protocol description, our compiler generates a smart contract that can then be completed by the programmer with the relevant business logic. The generated contracts rely on finite state machines to control endpoint invocations. As a proof of concept, we target Plutus, the contract programming language for the Cardano blockchain. Preliminary evaluation points to a 75% decrease in the size of the code that developers must write, coupled with an increase of reliability by enforcing the specified patterns of interaction. △ Less

Submitted 5 August, 2021; originally announced August 2021.

Comments: 20 pages, 9 figures

Polymorphic Lambda Calculus with Context-Free Session Types

Authors: Bernardo Almeida, Andreia Mordido, Peter Thiemann, Vasco T. Vasconcelos

Abstract: Context-free session types provide a ty** discipline for recursive structured communication protocols on bidirectional channels. They overcome the restriction of regular session type systems to tail recursive protocols. This extension enables us to implement serialisation and deserialisation of tree structures in a fully type-safe manner. We present the theory underlying the language FreeST 2,… ▽ More Context-free session types provide a ty** discipline for recursive structured communication protocols on bidirectional channels. They overcome the restriction of regular session type systems to tail recursive protocols. This extension enables us to implement serialisation and deserialisation of tree structures in a fully type-safe manner. We present the theory underlying the language FreeST 2, which features context-free session types in an extension of System F with linear types and a kind system to distinguish message types and channel types. The system presents some metatheoretical challenges, which we address, contractivity in the presence of polymorphism, a non-trivial equational theory on types, and decidability of type equivalence. We also establish standard results on type preservation, progress, and a characterisation of erroneous processes. △ Less

Submitted 2 August, 2022; v1 submitted 11 June, 2021; originally announced June 2021.

SafeRESTScript: Statically Checking REST API Consumers

Authors: Nuno Burnay, Antónia Lopes, Vasco T. Vasconcelos

Abstract: Consumption of REST services has become a popular means of invoking code provided by third parties, particularly in web applications. Nowadays programmers of web applications can choose TypeScript over JavaScript to benefit from static type checking that enables validating calls to local functions or to those provided by libraries. Errors in calls to REST services, however, can only be found at ru… ▽ More Consumption of REST services has become a popular means of invoking code provided by third parties, particularly in web applications. Nowadays programmers of web applications can choose TypeScript over JavaScript to benefit from static type checking that enables validating calls to local functions or to those provided by libraries. Errors in calls to REST services, however, can only be found at run-time. In this paper, we present SafeRESTScript (SRS, for short) a language that extends the support of static analysis to calls to REST services, with the ability to statically find common errors such as missing or invalid data in REST calls and misuse of the results from such calls. SafeRESTScript features a syntax similar to JavaScript and is equipped with (i) a rich collection of types (including objects, arrays and refinement types)and (ii) primitives to natively support REST calls that are statically validated against specifications of the corresponding APIs. Specifications are written in HeadREST, a language that also features refinement types and supports the description of semantic aspects of REST APIs in a style reminiscent of Hoare triples. We present SafeRESTScript and its validation system, based on a general-purpose verification tool (Boogie). The evaluation of SafeRESTScript and of the prototype implementations for its validator, available in the form of an Eclipse plugin, is also discussed. △ Less

Submitted 15 July, 2020; originally announced July 2020.

Mixed Sessions: the Other Side of the Tape

Authors: Filipe Casal, Andreia Mordido, Vasco T. Vasconcelos

Abstract: The original paper on Mixed Sessions introduce the side A of the tape: there is an encoding of classical sessions into mixed sessions. Here we present side B: there is a translation of (a subset of) mixed sessions into classical session types. We prove that the translation is a minimal encoding, according to the criteria put forward by Kouzapas, Pérez, and Yoshida. The original paper on Mixed Sessions introduce the side A of the tape: there is an encoding of classical sessions into mixed sessions. Here we present side B: there is a translation of (a subset of) mixed sessions into classical session types. We prove that the translation is a minimal encoding, according to the criteria put forward by Kouzapas, Pérez, and Yoshida. △ Less

Submitted 2 April, 2020; originally announced April 2020.

Comments: In Proceedings PLACES 2020, arXiv:2004.01062

Journal ref: EPTCS 314, 2020, pp. 46-60

Duality of Session Types: The Final Cut

Authors: Simon J. Gay, Peter Thiemann, Vasco T. Vasconcelos

Abstract: Duality is a central concept in the theory of session types. Since a flaw was found in the original definition of duality for recursive types, several other definitions have been published. As their connection is not obvious, we compare the competing definitions, discuss tradeoffs, and prove some equivalences. Some of the results are mechanized in Agda. Duality is a central concept in the theory of session types. Since a flaw was found in the original definition of duality for recursive types, several other definitions have been published. As their connection is not obvious, we compare the competing definitions, discuss tradeoffs, and prove some equivalences. Some of the results are mechanized in Agda. △ Less

Submitted 2 April, 2020; originally announced April 2020.

Comments: In Proceedings PLACES 2020, arXiv:2004.01062

ACM Class: D.3.1; D.3.3; F.3.3

Journal ref: EPTCS 314, 2020, pp. 23-33

Label-Dependent Session Types

Authors: Peter Thiemann, Vasco T. Vasconcelos

Abstract: Session types have emerged as a ty** discipline for communication protocols. Existing calculi with session types come equipped with many different primitives that combine communication with the introduction or elimination of the transmitted value. We present a foundational session type calculus with a lightweight operational semantics. It fully decouples communication from the introduction and… ▽ More Session types have emerged as a ty** discipline for communication protocols. Existing calculi with session types come equipped with many different primitives that combine communication with the introduction or elimination of the transmitted value. We present a foundational session type calculus with a lightweight operational semantics. It fully decouples communication from the introduction and elimination of data and thus features a single communication reduction, which acts as a rendezvous between senders and receivers. We achieve this decoupling by introducing label-dependent session types, a minimalist value-dependent session type system with subty**. The system is sufficiently powerful to simulate existing functional session type systems. Compared to such systems, label-dependent session types place fewer restrictions on the code. We further introduce primitive recursion over natural numbers at the type level, thus allowing to describe protocols whose behaviour depends on numbers exchanged in messages. An algorithmic type checking system is introduced and proved equivalent to its declarative counterpart. The new calculus showcases a novel lightweight integration of dependent types and linear ty**, with has uses beyond session type systems. △ Less

Submitted 11 November, 2019; v1 submitted 2 November, 2019; originally announced November 2019.

Comments: POPL 2020

Journal ref: Proc. ACM Program. Lang. 4, POPL, Article 67 (January 2020)

FreeST: Context-free Session Types in a Functional Language

Authors: Bernardo Almeida, Andreia Mordido, Vasco T. Vasconcelos

Abstract: FreeST is an experimental concurrent programming language. Based on a core linear functional programming language, it features primitives to fork new threads, and for channel creation and communication. A powerful type system of context-free session types governs the interaction on channels. The compiler builds on a novel algorithm for deciding type equivalence of context-free session types. This… ▽ More FreeST is an experimental concurrent programming language. Based on a core linear functional programming language, it features primitives to fork new threads, and for channel creation and communication. A powerful type system of context-free session types governs the interaction on channels. The compiler builds on a novel algorithm for deciding type equivalence of context-free session types. This abstract provides a gentle introduction to the language and discusses the validation process and runtime system. △ Less

Submitted 2 April, 2019; originally announced April 2019.

Comments: In Proceedings PLACES 2019, arXiv:1904.00396

ACM Class: D.3.2; D.3.3; D.3.4

Journal ref: EPTCS 291, 2019, pp. 12-23

Gradual Session Types

Authors: Atsushi Igarashi, Peter Thiemann, Yuya Tsuda, Vasco T. Vasconcelos, Philip Wadler

Abstract: Session types are a rich type discipline, based on linear types, that lifts the sort of safety claims that come with type systems to communications. However, web-based applications and microservices are often written in a mix of languages, with type disciplines in a spectrum between static and dynamic ty**. Gradual session types address this mixed setting by providing a framework which grants se… ▽ More Session types are a rich type discipline, based on linear types, that lifts the sort of safety claims that come with type systems to communications. However, web-based applications and microservices are often written in a mix of languages, with type disciplines in a spectrum between static and dynamic ty**. Gradual session types address this mixed setting by providing a framework which grants seamless transition between statically typed handling of sessions and any required degree of dynamic ty**. We propose Gradual GV as a gradually typed extension of the functional session type system GV. Following a standard framework of gradual ty**, Gradual GV consists of an external language, which relaxes the type system of GV using dynamic types, and an internal language with casts, for which operational semantics is given, and a cast-insertion translation from the former to the latter. We demonstrate type and communication safety as well as blame safety, thus extending previous results to functional languages with session-based communication. The interplay of linearity and dynamic types requires a novel approach to specifying the dynamics of the language. △ Less

Submitted 16 September, 2019; v1 submitted 15 September, 2018; originally announced September 2018.

Comments: Preprint of an article to appear in Journal of Functional Programming

Journal ref: J. Funct. Prog. 29 (2019) e17

Affine Sessions

Authors: Dimitris Mostrous, Vasco T. Vasconcelos

Abstract: Session types describe the structure of communications implemented by channels. In particular, they prescribe the sequence of communications, whether they are input or output actions, and the type of value exchanged. Crucial to any language with session types is the notion of linearity, which is essential to ensure that channels exhibit the behaviour prescribed by their type without interference i… ▽ More Session types describe the structure of communications implemented by channels. In particular, they prescribe the sequence of communications, whether they are input or output actions, and the type of value exchanged. Crucial to any language with session types is the notion of linearity, which is essential to ensure that channels exhibit the behaviour prescribed by their type without interference in the presence of concurrency. In this work we relax the condition of linearity to that of affinity, by which channels exhibit at most the behaviour prescribed by their types. This more liberal setting allows us to incorporate an elegant error handling mechanism which simplifies and improves related works on exceptions. Moreover, our treatment does not affect the progress properties of the language: sessions never get stuck. △ Less

Submitted 14 November, 2018; v1 submitted 8 September, 2018; originally announced September 2018.

ACM Class: F.3.2; F.4.1

Journal ref: Logical Methods in Computer Science, Volume 14, Issue 4 (November 15, 2018) lmcs:4815

Inferring Types for Parallel Programs

Authors: Francisco Martins, Vasco Thudichum Vasconcelos, Hans Hüttel

Abstract: The Message Passing Interface (MPI) framework is widely used in implementing imperative pro- grams that exhibit a high degree of parallelism. The PARTYPES approach proposes a behavioural type discipline for MPI-like programs in which a type describes the communication protocol followed by the entire program. Well-typed programs are guaranteed to be exempt from deadlocks. In this paper we describe… ▽ More The Message Passing Interface (MPI) framework is widely used in implementing imperative pro- grams that exhibit a high degree of parallelism. The PARTYPES approach proposes a behavioural type discipline for MPI-like programs in which a type describes the communication protocol followed by the entire program. Well-typed programs are guaranteed to be exempt from deadlocks. In this paper we describe a type inference algorithm for a subset of the original system; the algorithm allows to statically extract a type for an MPI program from its source code. △ Less

Submitted 10 April, 2017; originally announced April 2017.

Comments: In Proceedings PLACES 2017, arXiv:1704.02418

Journal ref: EPTCS 246, 2017, pp. 28-36

Proceedings Tenth Workshop on Programming Language Approaches to Concurrency- and Communication-cEntric Software

Authors: Vasco T. Vasconcelos, Philipp Haller

Abstract: PLACES 2017 (full title: Programming Language Approaches to Concurrency- and Communication-cEntric Software) is the tenth edition of the PLACES workshop series. After the first PLACES, which was affiliated to DisCoTec in 2008, the workshop has been part of ETAPS every year since 2009 and is now an established part of the ETAPS satellite events. PLACES 2017 was held on 29th April in Uppsala, Sweden… ▽ More PLACES 2017 (full title: Programming Language Approaches to Concurrency- and Communication-cEntric Software) is the tenth edition of the PLACES workshop series. After the first PLACES, which was affiliated to DisCoTec in 2008, the workshop has been part of ETAPS every year since 2009 and is now an established part of the ETAPS satellite events. PLACES 2017 was held on 29th April in Uppsala, Sweden. The workshop series was started in order to promote the application of novel programming language ideas to the increasingly important problem of develo** software for systems in which concurrency and communication are intrinsic aspects. This includes software for both multi-core systems and large-scale distributed and/or service-oriented systems. The scope of PLACES includes new programming language features, whole new programming language designs, new type systems, new semantic approaches, new program analysis techniques, and new implementation mechanisms. This volume consists of the papers accepted for presentation at the workshop. △ Less

Submitted 7 April, 2017; originally announced April 2017.

Journal ref: EPTCS 246, 2017

Deductive Verification of Parallel Programs Using Why3

Authors: César Santos, Francisco Martins, Vasco Thudichum Vasconcelos

Abstract: The Message Passing Interface specification (MPI) defines a portable message-passing API used to program parallel computers. MPI programs manifest a number of challenges on what concerns correctness: sent and expected values in communications may not match, resulting in incorrect computations possibly leading to crashes; and programs may deadlock resulting in wasted resources. Existing tools are… ▽ More The Message Passing Interface specification (MPI) defines a portable message-passing API used to program parallel computers. MPI programs manifest a number of challenges on what concerns correctness: sent and expected values in communications may not match, resulting in incorrect computations possibly leading to crashes; and programs may deadlock resulting in wasted resources. Existing tools are not completely satisfactory: model-checking does not scale with the number of processes; testing techniques wastes resources and are highly dependent on the quality of the test set. As an alternative, we present a prototype for a type-based approach to programming and verifying MPI like programs against protocols. Protocols are written in a dependent type language designed so as to capture the most common primitives in MPI, incorporating, in addition, a form of primitive recursion and collective choice. Protocols are then translated into Why3, a deductive software verification tool. Source code, in turn, is written in WhyML, the language of the Why3 platform, and checked against the protocol. Programs that pass verification are guaranteed to be communication safe and free from deadlocks. We verified several parallel programs from textbooks using our approach, and report on the outcome. △ Less

Submitted 19 August, 2015; originally announced August 2015.

Comments: In Proceedings ICE 2015, arXiv:1508.04595

ACM Class: D.2.4; F.3.1

Journal ref: EPTCS 189, 2015, pp. 128-142

Proceedings 7th Workshop on Programming Language Approaches to Concurrency and Communication-cEntric Software

Authors: Alastair F. Donaldson, Vasco T. Vasconcelos

Abstract: This volume contains the post-proceedings of PLACES 2014, the seventh Workshop on Programming Language Approaches to Concurrency and Communication-cEntric Software, which was held in Grenoble, France, on April 12th 2014, and co-located with ETAPS, the European Joint Conferences on Theory and Practice of Software. The PLACES workshop series aims to offer a forum where researchers from different fi… ▽ More This volume contains the post-proceedings of PLACES 2014, the seventh Workshop on Programming Language Approaches to Concurrency and Communication-cEntric Software, which was held in Grenoble, France, on April 12th 2014, and co-located with ETAPS, the European Joint Conferences on Theory and Practice of Software. The PLACES workshop series aims to offer a forum where researchers from different fields exchange new ideas on one of the central challenges for programming in the near future: the development of programming languages, methodologies and infrastructures where concurrency and distribution are the norm rather than a marginal concern. Previous editions of PLACES were held in Rome (2013), Tallin (2012), Saarbrueken (2011), Paphos (2010) and York (2009), all co-located with ETAPS, and the first PLACES was held in Oslo and co-located with DisCoTec (2008). The Program Committee, after a careful and thorough reviewing process, selected nine papers out of 12 submissions for presentation at the workshop and inclusion in this post-proceedings. Each submission was evaluated by three referees (with one paper receiving a fourth review), and the accepted papers were selected during a week-long electronic discussion. One of the nine accepted papers was conditionally accepted subject to a process of shepherding by a PC member, which was successful and led to the paper's full acceptance. In addition to the contributed papers, the workshop will feature an invited talk by Akash Lal, Microsoft Research India, entitled "Finding Concurrency Bugs Under Imprecise Harnesses". △ Less

Submitted 12 June, 2014; originally announced June 2014.

Journal ref: EPTCS 155, 2014

Towards deductive verification of MPI programs against session types

Authors: Eduardo R. B. Marques, Francisco Martins, Vasco T. Vasconcelos, Nicholas Ng, Nuno Martins

Abstract: The Message Passing Interface (MPI) is the de facto standard message-passing infrastructure for develo** parallel applications. Two decades after the first version of the library specification, MPI-based applications are nowadays routinely deployed on super and cluster computers. These applications, written in C or Fortran, exhibit intricate message passing behaviours, making it hard to statical… ▽ More The Message Passing Interface (MPI) is the de facto standard message-passing infrastructure for develo** parallel applications. Two decades after the first version of the library specification, MPI-based applications are nowadays routinely deployed on super and cluster computers. These applications, written in C or Fortran, exhibit intricate message passing behaviours, making it hard to statically verify important properties such as the absence of deadlocks. Our work builds on session types, a theory for describing protocols that provides for correct-by-construction guarantees in this regard. We annotate MPI primitives and C code with session type contracts, written in the language of a software verifier for C. Annotated code is then checked for correctness with the software verifier. We present preliminary results and discuss the challenges that lie ahead for verifying realistic MPI program compliance against session types. △ Less

Submitted 10 December, 2013; originally announced December 2013.

Comments: In Proceedings PLACES 2013, arXiv:1312.2218

Journal ref: EPTCS 137, 2013, pp. 103-113

Linearly Refined Session Types

Authors: Pedro Baltazar, Dimitris Mostrous, Vasco T. Vasconcelos

Abstract: Session types capture precise protocol structure in concurrent programming, but do not specify properties of the exchanged values beyond their basic type. Refinement types are a form of dependent types that can address this limitation, combining types with logical formulae that may refer to program values and can constrain types using arbitrary predicates. We present a pi calculus with assume an… ▽ More Session types capture precise protocol structure in concurrent programming, but do not specify properties of the exchanged values beyond their basic type. Refinement types are a form of dependent types that can address this limitation, combining types with logical formulae that may refer to program values and can constrain types using arbitrary predicates. We present a pi calculus with assume and assert operations, typed using a session discipline that incorporates refinement formulae written in a fragment of Multiplicative Linear Logic. Our original combination of session and refinement types, together with the well established benefits of linearity, allows very fine-grained specifications of communication protocols in which refinement formulae are treated as logical resources rather than persistent truths. △ Less

Submitted 17 November, 2012; originally announced November 2012.

Comments: In Proceedings LINEARITY 2012, arXiv:1211.3480

Journal ref: EPTCS 101, 2012, pp. 38-49

Modular session types for objects

Authors: Simon J. Gay, Nils Gesbert, António Ravara, Vasco T. Vasconcelos

Abstract: Session types allow communication protocols to be specified type-theoretically so that protocol implementations can be verified by static type checking. We extend previous work on session types for distributed object-oriented languages in three ways. (1) We attach a session type to a class definition, to specify the possible sequences of method calls. (2) We allow a session type (protocol) impleme… ▽ More Session types allow communication protocols to be specified type-theoretically so that protocol implementations can be verified by static type checking. We extend previous work on session types for distributed object-oriented languages in three ways. (1) We attach a session type to a class definition, to specify the possible sequences of method calls. (2) We allow a session type (protocol) implementation to be modularized, i.e. partitioned into separately-callable methods. (3) We treat session-typed communication channels as objects, integrating their session types with the session types of classes. The result is an elegant unification of communication channels and their session types, distributed object-oriented programming, and a form of typestate supporting non-uniform objects, i.e. objects that dynamically change the set of available methods. We define syntax, operational se-mantics, a sound type system, and a sound and complete type checking algorithm for a small distributed class-based object-oriented language with structural subty**. Static ty** guarantees that both sequences of messages on channels, and sequences of method calls on objects, conform to type-theoretic specifications, thus ensuring type-safety. The language includes expected features of session types, such as delegation, and expected features of object-oriented programming, such as encapsulation of local state. △ Less

Submitted 23 December, 2015; v1 submitted 24 May, 2012; originally announced May 2012.

Comments: Logical Methods in Computer Science (LMCS), International Federation for Computational Logic, 2015

Journal ref: Logical Methods in Computer Science, Volume 11, Issue 4 (December 16, 2015) lmcs:1613

Types for X10 Clocks

Authors: Francisco Martins, Vasco T. Vasconcelos, Tiago Cogumbreiro

Abstract: X10 is a modern language built from the ground up to handle future parallel systems, from multicore machines to cluster configurations. We take a closer look at a pair of synchronisation mechanisms: finish and clocks. The former waits for the termination of parallel computations, the latter allow multiple concurrent activities to wait for each other at certain points in time. In order to better un… ▽ More X10 is a modern language built from the ground up to handle future parallel systems, from multicore machines to cluster configurations. We take a closer look at a pair of synchronisation mechanisms: finish and clocks. The former waits for the termination of parallel computations, the latter allow multiple concurrent activities to wait for each other at certain points in time. In order to better understand these concepts we study a type system for a stripped down version of X10. The main result assures that well typed programs do not run into the errors identified in the X10 language reference, namely the ClockUseException. The study will open, we hope, doors to a more flexible utilisation of clocks in the X10 language. △ Less

Submitted 18 October, 2011; originally announced October 2011.

Comments: In Proceedings PLACES 2010, arXiv:1110.3853

ACM Class: D.1.3; D.2.4; D.3.1

Journal ref: EPTCS 69, 2011, pp. 111-129

Channels as Objects in Concurrent Object-Oriented Programming

Authors: Joana Campos, Vasco T. Vasconcelos

Abstract: There is often a sort of a protocol associated to each class, stating when and how certain methods should be called. Given that this protocol is, if at all, described in the documentation accompanying the class, current mainstream object-oriented languages cannot provide for the verification of client code adherence against the sought class behaviour. We have defined a class-based concurrent objec… ▽ More There is often a sort of a protocol associated to each class, stating when and how certain methods should be called. Given that this protocol is, if at all, described in the documentation accompanying the class, current mainstream object-oriented languages cannot provide for the verification of client code adherence against the sought class behaviour. We have defined a class-based concurrent object-oriented language that formalises such protocols in the form of usage types. Usage types are attached to class definitions, allowing for the specification of (1) the available methods, (2) the tests clients must perform on the result of methods, and (3) the object status - linear or shared - all of which depend on the object's state. Our work extends the recent approach on modular session types by eliminating channel operations, and defining the method call as the single communication primitive in both sequential and concurrent settings. In contrast to previous works, we define a single category for objects, instead of distinct categories for linear and for shared objects, and let linear objects evolve into shared ones. We introduce a standard sync qualifier to prevent thread interference in certain operations on shared objects. We formalise the language syntax, the operational semantics, and a type system that enforces by static ty** that methods are called only when available, and by a single client if so specified in the usage type. We illustrate the language via a complete example. △ Less

Submitted 18 October, 2011; originally announced October 2011.

Comments: In Proceedings PLACES 2010, arXiv:1110.3853

Journal ref: EPTCS 69, 2011, pp. 12-28

Type Inference for Deadlock Detection in a Multithreaded Polymorphic Typed Assembly Language

Authors: Vasco T. Vasconcelos, Francisco Martins, Tiago Cogumbreiro

Abstract: We previously developed a polymorphic type system and a type checker for a multithreaded lock-based polymorphic typed assembly language (MIL) that ensures that well-typed programs do not encounter race conditions. This paper extends such work by taking into consideration deadlocks. The extended type system verifies that locks are acquired in the proper order. Towards this end we require a langua… ▽ More We previously developed a polymorphic type system and a type checker for a multithreaded lock-based polymorphic typed assembly language (MIL) that ensures that well-typed programs do not encounter race conditions. This paper extends such work by taking into consideration deadlocks. The extended type system verifies that locks are acquired in the proper order. Towards this end we require a language with annotations that specify the locking order. Rather than asking the programmer (or the compiler's backend) to specifically annotate each newly introduced lock, we present an algorithm to infer the annotations. The result is a type checker whose input language is non-decorated as before, but that further checks that programs are exempt from deadlocks. △ Less

Submitted 5 February, 2010; v1 submitted 4 February, 2010; originally announced February 2010.

Journal ref: EPTCS 17, 2010, pp. 95-109