You are here: Home / Dissemination / Upscale Publications

Upscale Publications

Relaxed Linear References for Lock-free Data Structures

Authors: Elias Castegren and Tobias Wrigstad

Publication Year: 2017.

Abstract: Linear references are guaranteed to be free from aliases. This is a strong property that simplifies reasoning about programs and enables powerful optimisations, but it is also a property that is too strong for many applications. Notably, lock-free algorithms, which implement protocols that ensure safe, non-blocking concurrent access to data structures, are generally not typable with linear references because they rely on aliasing to achieve lock-freedom. This paper presents LOLCAT, a type system with a relaxed notion of linearity that allows an unbounded number of aliases to an object as long as at most one alias at a time owns the right to access the contents of the object. This ownership can be transferred between aliases, but can never be duplicated. LOLCAT types are powerful enough to type several lock-free data structures and give a compile-time guarantee of absence of data-races when accessing owned data. In particular, LOLCAT is able to assign types to the CAS (compare and swap) primitive that precisely describe how ownership is transferred across aliases, possibly across different threads. The paper introduces LOLCAT through a sound core procedural calculus, and shows how LOLCAT can be applied to three
fundamental lock-free data structures. It also discusses a prototype implementation which integrates LOLCAT with an object-oriented programming language.

 

Type-Assisted Automatic Garbage Collection for Lock-Free Data Structures

Authors: Albert Yang and Tobias Wrigstad

Publication Year: 2017.

Abstract: We introduce Isolde, an automatic garbage collection scheme designed specifically for managing memory in lock-free data structures, such as stacks, lists, maps and queues. Isolde exists as a plug-in memory manager, designed to sit on-top of another memory manager, and use its allocator and reclaimer (if exists). Isolde treats a lock-free data structure as a logical heap, isolated from the rest of the program. This allows garbage collection outside of Isolde to take place without affecting the lock-free data structure. Isolde further manages objects allocated on a Isolde heap in a fully concurrent manner, allowing garbage collection to incrementally remove garbage without stopping other threads doing work.

 

A Java Run-Time System for Actor-Based Cooperative Scheduling

Authors: Vlad Serbanescu, Frank de Boer, and Mahdi Jaghouri

Publication Year: 2017.

Abstract: Actor-based models of computation in general assume a run-to-completion mode of execution of the messages. The Abstract Behavioral Specification (ABS) Language extends the Actor-based model with a high-level synchronization mechanism which allows actors to suspend the execution of the current message and schedule in a cooperative manner another queued message. This extension is a powerful means for the expression and analysis of fine-grained run-time dependencies between messages. In this paper we introduce and evaluate a new run-time system in Java for the use of ABS as a full-fledged programming language. The main challenge is the development of an efficient and scalable implementation of cooperative scheduling. By means of a typical benchmark we evaluate our proposed solution and compare it to other thread-based implementations of cooperative scheduling.

Orca: Leveraging Types and Messaging for Fully Concurrent GC

Authors: Sylvan Clebsch, Juliana Franco, Sophia Drossopouloum, Albert Mingkun Yang, Tobias Wrigstad and Jan Vitek

Publication Year: 2017.

Abstract: Orca is a concurrent and parallel garbage collector for actor programs, which does not require any stop-the-world steps, or synchronisation mechanisms, and which has been designed to support zero-copy message passing and sharing of mutable data. Orca is part of the runtime of the actor-based language Pony. Pony’s runtime was co-designed with the Pony language. This co-design allowed to exploit certain language properties in order to optimise performance of garbage collection. Namely, Orca relies on the absence of race conditions in order to avoid read/write barriers, and it leverages the actor message passing for synchronisation among actors. This paper describes Pony, its type system, and the Orca garbage collection algorithm. An evaluation of the performance of Orca suggests that is fast and scalable for idiomatic workloads.

 

You Can Have it All: Abstraction and Good Cache Performance

Authors: Juliana Franco, Martin Hagelin, Tobias Wrigstad, Sophia Drossopoulou and Susan Eisenbach

Publication Year: 2017.

Abstract: On current architectures, the optimisation of an application's performance often involves data being stored according to access affinity --- what is accessed together should be stored together, rather than logical affinity --- what belongs together logically stays together. Such low level techniques lead to faster, but more error prone code, and end up tangling the program's logic with low-level data layout details. Our vision, which we call SHAPES, is that the layout of a data structure should be defined only once, upon instantiation, and the remainder of the code should be layout agnostic. This enables performance improvements while also guaranteeing memory safety, and supports the separation of program logic from low level concerns. In this paper we investigate how this vision can be supported by extending a programming language. We describe the core language features supporting this vision: classes can be customized to support different layouts, and layout information is carried around in types; the remaining source code is layout-unaware and the compiler emits layout-aware code. We then discuss our SHAPES implementation through a prototype library, which we also used for preliminary evaluations. Finally, we discuss how the core could be expanded so as to deliver SHAPES's full potential: the incorporation of compacting garbage collection, ad-hoc polymorphism and late binding, synchronization of representations of different collections, support for dynamic change of representation, etc.

 

Actors without Borders: Amnesty for Imprisoned State

Authors: Stephan Brandauer and Tobias Wrigstad

Publication Year: 2017.

Abstract: In concurrent systems, some form of synchronisation is typically needed to achieve data-race freedom, which is important for correctness and safety. In actor-based systems, messages are exchanged concurrently but executed sequentially by the receiving actor. By relying on isolation and non-sharing, an actor can access its own state without fear of data-races, and the internal behavior of an actor can be reasoned about sequentially. However, actor isolation is sometimes too strong to express useful patterns. For example, letting the iterator of a data-collection alias the internal structure of the collection allows a more efficient implementation than if each access requires going through the interface of the collection. With full isolation, in order to maintain sequential reasoning the iterator must be made part of the collection, which bloats the interface of the collection and means that a client must have access to the whole data-collection in order to use the iterator. In this paper, we propose a programming language construct that enables a relaxation of isolation but without sacrificing sequential reasoning. We formalise the mechanism in a simple lambda calculus with actors and passive objects, and show how an actor may leak parts of its internal state while ensuring that any interaction with this data is still synchronised.

 

Mining for Safety using Interactive Trace Analysis

Authors: Stephan Brandauer and Tobias Wrigstad

Publication Year: 2017.

Abstract: This paper presents the results of a trace-based study of object and reference properties on a subset of the DaCapo benchmark suite with the intent to uncover facts about programs that can be leveraged by type systems, compilers and run-times. In particular, we focus on aliasing, and immutability, based on their recent application in the literature. To facilitate analyses like this one, we previously created Spencer (http://spencer-t.racing, [8]), a web based tool and API that hosts dynamic trace data and enables researchers to query and analyse the data. In this paper we only use data that are openly accessible via Spencer’s API – all code written for this paper (not counting Spencer itself) amounts to 13 lines of bash and 260 lines of python to plot the results. We find that while Java allows aliasing and mutation by default, objects are often unique, unique on the heap, immutable, or stack-bound – 97.7% of objects fulfill at least one of these properties. Furthermore, uniqueness and immutability, or their absence, are class-properties, not object-properties: e.g.,, it is surprisingly rare for classes to produce both immutable and mutable instances. Although we use a different, more fine-grained, methodology, our findings confirm prior results.

 

Spencer: Interactive Heap Analysis for the Masses

Authors: Stephan Brandauer and Tobias Wrigstad

Publication Year: 2017.

Abstract: Programming language-design and run-time implementation require detailed knowledge about the programs that users want to implement. Acquiring this knowledge is hard, and there is little tool support to effectively estimate whether a proposed tradeoff actually makes sense in the context of real world applications. Ideally, knowledge about behaviour of “typical” programs is 1) easily obtainable, 2) easily reproducible, and 3) easily sharable. We present Spencer, an open source web service and API framework for dynamic analysis of a continuously growing set of traces of standard program corpora. Users do not obtain traces on their own, but can instead send queries to the web service that will be executed on a set of program traces. Queries are built in terms of a set of query combinators that present a high level interface for working with trace data. Since the framework is high level, and there is a hosted collection of recorded traces, queries are easy to implement. Since the data sets are shared by the research community, results are reproducible. Since the actual queries run on one (or many) servers that provide analysis as a service, obtaining results is possible on commodity hardware. Data in Spencer is meant to be obtained once, and analysed often, making the overhead of data collection mostly irrelevant. This allows Spencer to collect more data than traditional tracing tools can afford within their performance budget. Results in Spencer are cached, making complicated analyses that build on cached primitive queries speedy.

  

On Futures for Streaming Data in ABS

Authors: Keyvan Azadbakht, Nikolaos Bezirgiannis, and Frank S. de Boer

Publication Year: 2017.

Abstract: Many modern distributed software applications require a continuous interaction between their components exploiting streaming data from the server to the client. The Abstract Behavioral Specification (ABS) language has been developed for the modeling and analysis of distributed systems. In ABS, concurrent objects communicate by calling each other's methods asynchronously. Return values are communicated asynchronously too via the return statement and so-called futures. In this paper, we extend the basic ABS model of asynchronous method invocation and return in order to support the streaming of data. We introduce the notion of a ``Future-based Data Stream'' to extend the ABS. The application of this notion and its impact on performance are illustrated by means of a case study in the domain of social networks simulation.

 

Distributed Network Generation Based on Preferential Attachment in ABS

Authors: Keyvan Azadbakht, Nikolaos Bezirgiannis, and Frank S. de Boer

Publication Year: 2017.

Abstract: Generation of social networks using Preferential Attachment (PA) mechanism is proposed in Barabasi-Albert model. In this mechanism, new nodes are introduced to the network sequentially and they attach to the existing nodes preferentially where the preference can be based on the degree of the existing nodes. PA is a classical model with a natural intuition, great explanatory power and interesting mathematical properties. Some of these properties only appear in large-scale networks. However generation of such extra-large networks can be challenging due to memory limitations. In this paper, we investigate a distributed-memory approach for PA-based network generation which is scalable and which avoids low-level synchronization mechanisms thanks to utilizing a powerful programming model and proper programming constructs.

 

Monitoring Networks through Multiparty Session Types

Authors: Laura Bocchia, Tzu-chun Chenb, Romain Demangeonc, Kohei Hondad and Nobuko Yoshida

Publication Year: 2017.

Abstract: In large-scale distributed infrastructures, applications are realised through communications among distributed components. The need for methods for assuring safe interactions in such environments is recognised, however the existing frameworks, relying on centralised verification or restricted specification methods, have limited applicability. This paper proposes a new theory of monitored π-calculus with dynamic usage of multiparty session types (MPST), offering a rigorous foundation for safety assurance of distributed components which asynchronously communicate through multiparty sessions. Our theory establishes a framework for semantically precise decentralised run-time enforcement and provides reasoning principles over monitored distributed applications, which complement existing static analysis techniques. We introduce asynchrony through the means of explicit routers and global queues, and propose novel equivalences between networks, that capture the notion of interface equivalence, i.e. equating networks offering the same services to a user. We illustrate our static-dynamic analysis system with an ATM protocol as a running example and justify our theory with results: satisfaction equivalence, local/global safety and transparency, and session fidelity.

 

Timed Runtime Monitoring for Multiparty Conversations

Authors: Rumyana Neykova, Laura Bocchi and Nobuko Yoshida

Publication Year: 2017.

Abstract: We propose a dynamic verification framework for protocols in real-time distributed systems. The framework is based on Scribble, a tool-chain for design and verification of choreographies based on multiparty session types, which we have developed with our industrial partners. Drawing from recent work on multiparty session types for real-time interactions, we extend Scribble with clocks, resets, and clock predicates in order to constrain the times in which interactions occur. We present a timed API for Python to program distributed implementations of Scribble specifications. A dynamic verification framework ensures the safe execution of applications written with our timed API: we have implemented dedicated runtime monitors that check that each interaction occurs at a correct timing with respect to the corresponding Scribble specification. To demonstrate the practicality of the proposed framework, we express and verify four categories of widely used temporal patterns from use cases in literature. We analyse the performance of our implementation via benchmarking and show negligible overhead.

 

Explicit Connection Actions in Multiparty Session Types

Authors: Raymond Hu and Nobuko Yoshida

Publication Year: 2017.

Abstract: This work extends asynchronous multiparty session types (MPST) with explicit connection actions to support protocols with optional and dynamic participants. The actions by which endpoints are connected and disconnected are a key element of real-world protocols that is not treated in existing MPST works. In addition, the use cases motivating explicit connections often require a more relaxed form of multiparty choice: these extensions do not satisfy the conservative restrictions used to ensure safety in standard syntactic MPST. Instead, we develop a modelling-based approach to validate MPST safety and progress for these enriched protocols. We present a toolchain implementation, for distributed programming based on our extended MPST in Java, and a core formalism, demonstrating the soundness of our approach. We discuss key implementation issues related to the proposed extensions: a practical treatment of choice subtyping for MPST progress, and multiparty correlation of dynamic binary connections.

Fencing off Go: Liveness and Safety for Channel-Based Programming

Authors: Julien Lange Nicholas Ng Bernardo Toninho Nobuko Yoshida

Publication Year: 2017.

Abstract: Go is a production-level statically typed programming language whose design features explicit message-passing primitives and lightweight threads, enabling (and encouraging) programmers to develop concurrent systems where components interact through communication more so than by lock-based shared memory concurrency. Go can only detect global deadlocks at runtime, but provides no compile-time protection against all too common communication mismatches or partial deadlocks. This work develops a static verification framework for bounded liveness and safety in Go programs, able to detect communication errors and partial deadlocks in a general class of realistic concurrent programs, including those with dynamic channel creation and infinite recursion. Our approach infers from a Go program a faithful representation of its communication patterns as a behavioural type. By checking a syntactic restriction on channel usage, dubbed fencing, we ensure that programs are made up of finitely many different communication patterns that may be repeated infinitely many times. This restriction allows us to implement bounded verification procedures (akin to bounded model checking) to check for liveness and safety in types which in turn approximates liveness and safety in Go programs. We have implemented a type inference and liveness and safety checks in a tool-chain and tested it against publicly available Go programs.

 

Let It Recover: Multiparty Protocol-Induced Recovery

Authors: Rumyana Neykova and Nobuko Yoshida

Publication Year: 2017.

Abstract: Fault-tolerant communication systems rely on recovery strategies which are often error-prone (e.g. a programmer manually specifies recovery strategies) or inefficient (e.g. the whole system is restarted from the beginning). This paper proposes a static analysis based on multiparty session types that can efficiently compute a safe global state from which a system of interacting processes should be recovered. We statically analyse the communication flow of a program, given as a multiparty protocol, to extract the causal dependencies between processes and to localise failures. We formalise our recovery algorithm and prove its safety. A recovered communication system is free from deadlocks, orphan messages and reception errors. Our recovery algorithm incurs less communication cost (only affected processes are notified) and overall execution time (only required states are repeated). On top of our analysis, we design and implement a runtime framework in Erlang where failed processes and their dependencies are soundly restarted from a computed safe state. We evaluate our recovery framework on messagepassing benchmarks and a use case for crawling webpages. The experimental results indicate our framework outperforms a built-in static recovery strategy in Erlang when a part of the protocol can be safely recovered.

 

Multiparty Session Actors

Authors: RUMYANA NEYKOVA AND NOBUKO YOSHIDA

Publication Year: 2017.

Abstract: Actor coordination armoured with a suitable protocol description language has been a pressing problem in the actors community. We study the applicability of multiparty session type (MPST) protocols for verification of actor programs. We incorporate sessions to actors by introducing minimum additions to the model such as the notion of actor roles and protocol mailboxes. The framework uses Scribble, which is a protocol description language based on multiparty session types. Our programming model supports actor-like syntax and runtime verification mechanism guaranteeing communication safety of the participating entities. An actor can implement multiple roles in a similar way as an object can implement multiple interfaces. Multiple roles allow for cooperative inter-concurrency in a single actor. We demonstrate our framework by designing and implementing a session actor library in Python and its runtime verification mechanism. Benchmark results demonstrate that the runtime checks induce negligible overhead. We evaluate the applicability of our verification framework to specify actor interactions by implementing twelve examples from an actor benchmark suit.

 

Multiparty session types as coherence proofs

Authors: Marco Carbone, Fabrizio Montesi, Carsten Schürmann and Nobuko Yoshida

Publication Year: 2017.

Abstract: We propose a Curry–Howard correspondence between a language for programming multiparty sessions and a generalisation of Classical Linear Logic (CLL). In this framework, propositions correspond to the local behaviour of a participant in a multiparty session type, proofs to processes, and proof normalisation to executing communications. Our key contribution is generalising duality, from CLL, to a new notion of n-ary compatibility, called coherence. Building on coherence as a principle of compositionality, we generalise the cut rule of CLL to a new rule for composing many processes communicating in a multiparty session. We prove the soundness of our model by showing the admissibility of our new rule, which entails deadlock-freedom via our correspondence.

 

On the Preciseness of Subtyping in Session Types

Authors: TZU-CHUN CHEN, MARIANGIOLA DEZANI-CIANCAGLINI, ALCESTE SCALAS, AND NOBUKO YOSHIDA

Publication Year: 2017.

Abstract: Subtyping in concurrency has been extensively studied since early 1990s as one of the most interesting issues in type theory. The correctness of subtyping relations has been usually provided as the soundness for type safety. The converse direction, the completeness, has been largely ignored in spite of its usefulness to define the largest subtyping relation ensuring type safety. This paper formalises preciseness (i.e. both soundness and completeness) of subtyping for mobile processes and studies it for the synchronous and the asynchronous session calculi. We first prove that the well-known session subtyping, the branching-selection subtyping, is sound and complete for the synchronous calculus. Next we show that in the asynchronous calculus, this subtyping is incomplete for type-safety: that is, there exist session types T and S such that T can safely be considered as a subtype of S, but T 6 S is not derivable by the subtyping. We then propose an asynchronous subtyping system which is sound and complete for the asynchronous calculus. The method gives a general guidance to design rigorous channel-based subtypings respecting desired safety properties. Both the synchronous and the asynchronous calculus are first considered with linear channels only, and then they are extended with session initialisations and communications of expressions (including shared channels).

 

On the Undecidability of Asynchronous Session Subtyping

Authors: Julien Lange and Nobuko Yoshida

Publication Year: 2017.

Abstract: Asynchronous session subtyping has been studied extensively in [9, 10, 28–31] and applied in [23, 32, 33, 35]. An open question was whether this subtyping relation is decidable. This paper settles the question in the negative. To prove this result, we first introduce a new subclass of two-party communicating finite-state machines (CFSMs), called asynchronous duplex (ADs), which we show to be Turing complete. Secondly, we give a compatibility relation over CFSMs, which is sound and complete wrt. safety for ADs, and is equivalent to the asynchronous subtyping. Then we show that the halting problem reduces to checking whether two CFSMs are in the relation. In addition, we show the compatibility relation to be decidable for three sub-classes of ADs.

 

Session-ocaml: a session-based library with polarities and lenses

Authors: Keigo Imai , Nobuko Yoshida and Shoji Yuen

Publication Year: 2017.

Abstract: We propose session-ocaml, a novel library for session-typed concurrent/distributed programming in OCaml. Our technique solely relies on parametric polymorphism, which can encode core session type structures with strong static guarantees. Our key ideas are: (1) polarised session types, which give an alternative formulation of duality enabling OCaml to automatically infer an appropriate session type in a session with a reasonable notational overhead; and (2) a parameterised monad with a data structure called ‘slots’ manipulated with lenses, which can statically enforce session linearity and delegations. We show applications of session-ocaml including a travel agency usecase and an SMTP protocol.

 

Towards a Categorical Representation of Reversible Event Structures

Authors: Eva Graversen, Iain Phillips and Nobuko Yoshida

Publication Year: 2017.

Abstract: We study categories for reversible computing, focussing on reversible forms of event structures. Event structures are a well-established model of true concurrency. There exist a number of forms of event structures, including prime event structures, asymmetric event structures, and general event structures. More recently, reversible forms of these types of event structures have been defined. We formulate corresponding categories and functors between them. We show that products and coproducts exist in many cases. In most work on reversible computing, including reversible process calculi, a cause-respecting condition is posited, meaning that the cause of an event may not be reversed before the event itself. Since reversible event structures are not assumed to be cause-respecting in general, we also define cause-respecting subcategories of these event structures. Our longer-term aim is to formulate event structure semantics for reversible process calculi.

 

Multiparty Session Types, Beyond Duality

Authors: Alceste Scalas and Nobuko Yoshida

Publication Year: 2016.

Abstract: The rise of multicore computers has hastened the advent of multifarious abstractions to facilitate the construction of parallel programs. This paper presents another: the vat. A vat is like a variable, but it has various actions attached to it that can block, transform and react to changes to the vat. Vats can be combined together in various ways, linking the behaviours of the vats together, resulting in various synchronisation mechanisms. Vats are powerful enough to encode (part of) many existing mechanisms including promises, condition variables, LVars and reactive programming.

 

Certifying data in multiparty session types

Authors: Bernardo Toninho and Nobuko Yoshida

Publication Year: 2016.

Abstract: Multiparty session types (MPST) are a typing discipline for ensuring the coordination of multi-agent communication in concurrent and distributed programs. The original MPST framework mainly focuses on the communication aspects of concurrency, unable to capture important data invariants in communicating programs. This work introduces value dependent types to the MPST framework in order to increase its expressiveness for certifying invariants of data exchanged among multiple participants. The key idea is to impose constraints on the exchanged data, which is explicitly witnessed at runtime by proof objects. The enriched MPST framework provides programmers with a precise global description of the interaction and data dependent patterns, from which local (data dependent) descriptions can be automatically generated for each endpoint, faithfully capturing at a local level the global data constraints. The framework ensures the absence of communication errors and guarantees communication progress in well-typed multiparty sessions. We also develop an extension of value dependencies based on proof irrelevance that enables the selective erasure of proof objects at runtime.

 

Multi-Threaded Actors

Authors: Keyvan Azadbakht, Frank S. de Boer and Vlad Serbanescu

Publication Year: 2016.

Abstract: In this paper we introduce a new programming model of multi-threaded actors which feature the parallel processing of their messages. In this model an actor consists of a group of active objects which share a message queue. We provide a formal operational semantics, and a description of a Java-based implementation for the basic programming abstractions describing multi-threaded actors. Finally, we evaluate our proposal by means of an example application.

 

A High-Level and Scalable Approach for Generating Scale-Free Graphs using Active Objects

Authors: Keyvan Azadbakht, Nikolaos Bezirgiannis, Frank S. de Boer and Sadegh Aliakbary

Publication Year: 2016.

Abstract: The Barabasi-Albert model (BA) is designed to generate scale-free networks using the preferential attachment mechanism. In the preferential attachment (PA) model, new nodes are sequentially introduced to the network and they attach preferentially to existing nodes. PA is a classical model with a natural intuition, great explanatory power and a simple mechanism. Therefore, PA is widely-used for network generation. However the sequential mechanism used in the PA model makes it an inefficient algorithm. The existing parallel approaches, on the other hand, suffer from either changing the original model or explicit complex low-level synchronization mechanisms. In this paper we investigate a high-level Actor-based model of the parallel algorithm of network generation and its scalable multicore implementation in Haskell.

 

A Java-Based Distributed Approach for Generating Large-Scale Social Network Graphs

Authors: Vlad Serbanescu, Keyvan Azadbakht and Frank de Boer

Publication Year: 2016.

Abstract: Barabasi–Albert model, which is based on preferential attachment (PA), is one of the most commonly used models to produce artificial networks, because of its explanatory power, conceptual simplicity, and interesting mathematical properties. Nevertheless the large number of nodes in such graphs may not fit in the memory on one machine. The need for efficient solutions which provide scalability also requires more computational resources as well as implementation considerations. As such, distribution and synchronization are two main challenges. In this chapter, we investigate as a case study a distributed solution for PA-based graph generation in Java which avoids low level synchronization management, thanks to the notion of cooperative scheduling and futures.

 

A Design Pattern for Optimizations in Data Intensive Applications using ABS and JAVA 8

Authors: V. Serbanescu, K. Azadbakht, F. de Boer, C. Nagarajagowda and B. Nobakht

Publication Year: 2016.

Abstract: Cloud environments have become a standard method for enterprises to offer their applications by means of web-services, data management systems or simply renting out computing resources. In our previous work we presented how we can use a modeling language together with the new features of JAVA 8 to overcome certain drawbacks of data structures and synchronization mechanisms in parallel applications. We extend this solution into a design pattern that allows application-specific optimizations in a distributed setting. We validate this integration using our previous case study of the Prime Sieve of Eratosthenes and illustrate the performance improvements in terms of speed-up and memory consumption.

 

Reference Capabilities for Concurrency Control

Authors: Elias Castegren and Tobias Wrigstad

Publication Year: 2016.

Abstract: The proliferation of shared mutable state in object-oriented programming complicates software development as two seemingly unrelated operations may interact via an alias and produce unexpected results. In concurrent programming this manifests itself as data-races. Concurrent object-oriented programming further suffers from the fact that code that warrants synchronisation cannot easily be distinguished from code that does not. The burden is placed solely on the programmer to reason about alias freedom, sharing across threads and side-effects to deduce where and when to apply concurrency control, without inadvertently blocking parallelism. This paper presents a reference capability approach to concurrent and parallel object-oriented programming where all uses of aliases are guaranteed to be data-race free. The static type of an alias describes its possible sharing without using explicit ownership or effect annotations. Type information can express non-interfering deterministic parallelism without dynamic concurrency control, thread-locality, lock-based schemes, and guarded-by relations giving multi-object atomicity to nested data structures. Unification of capabilities and traits allows trait-based reuse across multiple concurrency scenarios with minimal code duplication. The resulting system brings together features from a wide range of prior work in a unified way.

 

Towards Enabling Low-Level Memory Optimisations at the High-Level with Ownership-like Annotations

Authors: Juliana Franco, Tobias Wrigstad and Sophia Drossopoulou

Publication Year: 2016.

Abstract: In modern architectures, due to the huge gap between CPU performance and memory bandwidth, an application’s performance highly depends on the speed at which the system is able to deliver data to operate on. The placement of data in memory affects the number of cache misses, and thus the overall speed of the application. To address this, pooling and splitting are two techniques that allow to group or split data in memory, according to whether they are usually accessed together or separately. However, these are either low-level optimisations, or outside the control of the programmer. We propose OHMM, an object-oriented programming language that uses ownership-like annotations to express high-level constraints on how objects should be placed in memory. These annotations will allow the runtime to allocate objects using pooling and splitting, and thus lead to efficient data accesses. In this short paper, we explain OHMM through an example, show how the objects will be laid out, and informally argue the benefits in terms of cache performance.

Kappa: Insights, Current Status and Future Work

Authors: Elias Castegren and Tobias Wrigstad

Publication Year: 2016.

Abstract: KAPPA is a type system for safe concurrent object-oriented programming using reference capabilities. It uses a combination of static and dynamic techniques to guarantee data-race freedom, and, for a certain subset of the system, non-interference (and thereby deterministic parallelism). It combines many features from previous work on alias management, such as substructural types, regions, ownership types, and fractional permissions, and brings them together using a unified set of primitives. In this extended abstract we show how KAPPA’s capabilities express variations of the aforementioned concepts, discuss the main insights from working with KAPPA, present the current status of the implementation of KAPPA in the context of the actor language Encore, and discuss ongoing and future work.

 

Reference Capabilities for Trait Based Reuse and Concurrency Control 

Authors: Elias Castegren and Tobias Wrigstad

Publication Year: 2016.

Abstract: The proliferation of shared mutable state in object-oriented programming complicates software development as two seemingly unrelated operations may interact via an alias and produce unexpected results. In concurrent programming this manifests itself as data-races. Concurrent objectoriented programming further suffers from the fact that code that warrants synchronisation cannot easily be distinguished from code that does not. The burden is placed solely on the programmer to reason about alias freedom, sharing across threads and side-effects to deduce where and when to apply concurrency control, without inadvertently blocking parallelism. This paper presents a reference capability approach to concurrent and parallel object-oriented programming where all uses of aliases are guaranteed to be data-race free. The static type of an alias describes its possible sharing without using explicit ownership or effect annotations. Type information can express non-interfering deterministic parallelism without dynamic concurrency control, thread-locality, lock-based schemes, and guarded-by relations giving multi-object atomicity to nested data structures. Unification of capabilities and traits allows trait-based reuse across multiple concurrency scenarios with minimal code duplication. The resulting system brings together features from a wide range of prior work in a unified way.

 

LOLCAT: Relaxed Linear References for Lock-free Programming

Authors: Elias Castegren and Tobias Wrigstad

Publication Year: 2016.

Abstract: A linear reference is a reference guaranteed to be unaliased. This is a powerful property that simplifies reasoning about programs, but is also a property that is too strong for certain applications. For example, lock-free algorithms, which implement protocols to ensure safe concurrent access to data structures, are generally not typable with linear references as they involve sharing of mutable state. This paper presents a type system with a relaxed notion of linearity that allows an unbounded number of aliases to an object as long as at most one alias at a time owns the right to access the contents of the object. This ownership can be transferred between aliases, but can never be duplicated. The resulting language is flexible enough to express several lock-free algorithms and at the same time powerful enough to guarantee the absence of data-races when accessing owned data. The language is formalised and proven sound, and is also available as a prototype implementation.

 

Actors and Hot Objects

Authors: Tobias Wrigstad and Thorbiorn Fritzon

Publication Year: 2016.

Abstract: We present Hot Objects, actors which logically support processing of multiple messages in parallel, in the Encore programming language. The internal behaviour of Hot objects is encapsulated inside an asynchronous interface. We discuss compositionality of Hot Objects and the reintroduction of locks into actor-based systems.

 

Types for CAS: Relaxed Linearity with Ownership Transfer

Authors: Elias Castegren and Tobias Wrigstad

Publication Year: 2016.

Abstract: This extended abstract overviews work on a type system for lock-free programming based on compare-and-swap. The type system prevents atomicity violations in lock-free programs, where insertion and removal of objects from a linked structure would be subject to data-races breaking linearity of ownership. The type system has successfully been applied to a small number of lock-free data structures.

 

Disjointness Domains for Fine-Grained Aliasing

Authors: Stephan Brandauer, Dave Clarke, and Tobias Wrigstad

Publication Year: 2015.

Abstract: In large-scale distributed infrastructures, applications are realised through communications among distributed components. The need for methods for assuring safe interactions in such environments is recognised, however the existing frameworks, relying on centralised verification or restricted specification methods, have limited applicability. This paper proposes a new theory of monitored π-calculus with dynamic usage of multiparty session types (MPST), offering a rigorous foundation for safety assurance of distributed components which asynchronously communicate through multiparty sessions. Our theory establishes a framework for semantically precise decentralised run-time enforcement and provides reasoning principles over monitored distributed applications, which complement existing static analysis techniques. We introduce asynchrony through the means of explicit routers and global queues, and propose novel equivalences between networks, that capture the notion of interface equivalence, i.e. equating networks offering the same services to a user. We illustrate our static-dynamic analysis system with an ATM protocol as a running example and justify our theory with results: satisfaction equivalence, local/global safety and transparency, and session fidelity.

Characteristic bisimulation for higher-order session processes

Authors: Dimitrios Kouzapas, Jorge A. Pérez and Nobuko Yoshida

Publication Year: 2017.

Abstract: For higher-order (process) languages, characterising contextual equivalence is a long-standing issue. In the setting of a higher-order π-calculus with session types, we develop characteristic bisimilarity, a typed bisimilarity which fully characterises contextual equivalence. To our knowledge, ours is the first characterisation of its kind. Using simple values inhabiting (session) types, our approach distinguishes from untyped methods for characterising contextual equivalence in higher-order processes: we show that observing as inputs only a precise finite set of higher-order values suffices to reason about higher-order session processes. We demonstrate how characteristic bisimilarity can be used to justify optimisations in session protocols with mobile code communication.

Type Checking Liveness for Collaborative Processes with Bounded and Unbounded Recursion

Authors: Søren Debois1 , Thomas Hildebrandt1 , Tijs Slaats1,2 , and Nobuko Yoshida3

Publication Year: 2016.

Abstract: We present the first session typing system guaranteeing response liveness properties for possibly non-terminating communicating processes. The types augment the branch and select types of the standard binary session types with a set of required responses, indicating that whenever a particular label is selected, a set of other labels, its responses, must eventually also be selected. We prove that these extended types are strictly more expressive than standard session types. We provide a type system for a process calculus similar to a subset of collaborative BPMN processes with internal (data-based) and external (event-based) branching, message passing, bounded and unbounded looping. We prove that this type system is sound, i.e., it guarantees request-response liveness for dead-lock free processes. We exemplify the use of the calculus and type system on a concrete example of an infinite state system.

 

Static Deadlock Detection for Concurrent Go by Global Session Graph Synthesis

Authors: Nicholas Ng and Nobuko Yoshida

Publication Year: 2016.

Abstract: Go is a programming language developed at Google, with channelbased concurrent features based on CSP. Go can detect global communication deadlocks at runtime when all threads of execution are blocked, but deadlocks in other paths of execution could be undetected. We present a new static analyser for concurrent Go code to find potential communication errors such as communication mismatch and deadlocks at compile time. Our tool extracts the communication operations as session types, which are then converted into Communicating Finite State Machines (CFSMs). Finally, we apply a recent theoretical result on choreography synthesis to generate a global graph representing the overall communication pattern of a concurrent program. If the synthesis is successful, then the program is free from communication errors. We have implemented the technique in a tool, and applied it to analyse common Go concurrency patterns and an open source application with over 700 lines of code.

Reversing Single Sessions

Authors: Francesco Tiezzi and Nobuko Yoshida

Publication Year: 2016.

Abstract: Session-based communication has gained a widespread acceptance in practice as a means for developing safe communicating systems via structured interactions. In this paper, we investigate how these structured interactions are affected by reversibility, which provides a computational model allowing executed interactions to be undone. In particular, we provide a systematic study of the integration of different notions of reversibility in both binary and multiparty single sessions. The considered forms of reversibility are: one for completely reversing a given session with one backward step, and another for also restoring any intermediate state of the session with either one backward step or multiple ones. We analyse the costs of reversing a session in all these different settings. Our results show that extending binary single sessions to multiparty ones does not affect the reversibility machinery and its costs.

 

Lightweight Session Programming in Scala

Authors: Alceste Scalas and Nobuko Yoshida

Publication Year: 2016.

Abstract: Designing, developing and maintaining concurrent applications is an error-prone and time-consuming task; most difficulties arise because compilers are usually unable to check whether the inputs/outputs performed by a program at runtime will adhere to a given protocol specification. To address this problem, we propose lightweight session programming in Scala: we leverage the native features of the Scala type system and standard library, to introduce (1) a representation of session types as Scala types, and (2) a library, called lchannels, with a convenient API for session-based programming, supporting local and distributed communication. We generalise the idea of Continuation-Passing Style Protocols (CPSPs), studying their formal relationship with session types. We illustrate how session programming can be carried over in Scala: how to formalise a communication protocol, and represent it using Scala classes and lchannels, letting the compiler help spotting protocol violations. We attest the practicality of our approach with a complex use case, and evaluate the performance of lchannels with a series of benchmarks.

 

Denotational and Operational Preciseness of Subtyping: A Roadmap

Authors: Mariangiola Dezani-Ciancaglini, Silvia Ghilezan, Svetlana Jaksic, Jovanka Pantovic and Nobuko Yoshida

Publication Year: 2016.

Abstract: The notion of subtyping has gained an important role both in theoretical and applicative domains: in lambda and concurrent calculi as well as in object-oriented programming languages. The soundness and the completeness, together referred to as the preciseness of subtyping, can be considered from two different points of view: denotational and operational. The former preciseness is based on the denotation of a type, which is a mathematical object describing the meaning of the type in accordance with the denotations of other expressions from the language. The latter preciseness has been recently developed with respect to type safety, i.e. the safe replacement of a term of a smaller type when a term of a bigger type is expected. The present paper shows that standard proofs of operational preciseness imply denotational preciseness and gives an overview on this subject.

Effects as Sessions, Sessions as Effects

Authors: Dominic Orchard and Nobuko Yoshida

Publication Year: 2016.

Abstract: Effect and session type systems are two expressive behavioural type systems. The former is usually developed in the context of the λ- calculus and its variants, the latter for the π-calculus. In this paper we explore their relative expressive power. Firstly, we give an embedding from PCF, augmented with a parameterised effect system, into a session-typed π-calculus (session calculus), showing that session types are powerful enough to express effects. Secondly, we give a reverse embedding, from the session calculus back into PCF, by instantiating PCF with concurrency primitives and its effect system with a session-like effect algebra; effect systems are powerful enough to express sessions. The embedding of session types into an effect system is leveraged to give a new implementation of session types in Haskell, via an effect system encoding. The correctness of this implementation follows from the second embedding result. We also discuss various extensions to our embeddings

 

Certifying data in multiparty session types

Authors: Bernardo Toninho and Nobuko Yoshida

Publication Year: 2016.

Abstract: Multiparty session types (MPST) are a typing discipline for ensuring the coordination of multi-agent communication in concurrent and distributed programs. The original MPST framework mainly focuses on the communication aspects of concurrency, unable to capture important data invariants in communicating programs. This work introduces value dependent types to the MPST framework in order to increase its expressiveness for certifying invariants of data exchanged among multiple participants. The key idea is to impose constraints on the exchanged data, which is explicitly witnessed at runtime by proof objects. The enriched MPST framework provides programmers with a precise global description of the interaction and data dependent patterns, from which local (data dependent) descriptions can be automatically generated for each endpoint, faithfully capturing at a local level the global data constraints. The framework ensures the absence of communication errors and guarantees communication progress in well-typed multiparty sessions. We also develop an extension of value dependencies based on proof irrelevance that enables the selective erasure of proof objects at runtime.

 

On the Relative Expressiveness of Higher-Order Session Processes

Authors: Dimitrios Kouzapas, Jorge A. Perez, and Nobuko Yoshida

Publication Year: 2016.

Abstract: By integrating constructs from the λ-calculus and the π-calculus, in higher-order process calculi exchanged values may contain processes. This paper studies the relative expressiveness of HOπ, the higher-order π-calculus in which communications are governed by session types. Our main discovery is that HO, a subcalculus of HOπ which lacks name-passing and recursion, can serve as a new core calculus for session-typed higher-order concurrency. By exploring a new bisimulation for HO, we show that HO can encode HOπ fully abstractly (up to typed contextual congruence) more precisely and efficiently than the first-order session π-calculus (π). Overall, under session types, HOπ, HO, and π are equally expressive; but HOπ and HO are more tightly related than HOπ and π.

 

Hybrid Session Verification through Endpoint API Generation

Authors: Raymond Hu and Nobuko Yoshida

Publication Year: 2016.

Abstract: The rise of multicore computers has hastened the advent of multifarious abstractions to facilitate the construction of parallel programs. This paper presents another: the vat. A vat is like a variable, but it has various actions attached to it that can block, transform and react to changes to the vat. Vats can be combined together in various ways, linking the behaviours of the vats together, resulting in various synchronisation mechanisms. Vats are powerful enough to encode (part of) many existing mechanisms including promises, condition variables, LVars and reactive programming.

 

Characteristic Formulae for Session Types

Authors: Julien Lange, Nobuko Yoshida

Publication Year: 2016.

Abstract: Subtyping is a crucial ingredient of session type theory and its applications, notably to programming language implementations. In this paper, we study effective ways to check whether a session type is a subtype of another by applying a characteristic formulae approach to the problem. Our core contribution is an algorithm to generate a modal µ-calculus formula that characterises all the supertypes (or subtypes) of a given type. Subtyping checks can then be off-loaded to model checkers, thus incidentally yielding an efficient algorithm to check safety of session types, soundly and completely. We have implemented our theory and compared its cost with other classical subtyping algorithms.


An Operational Semantics of Cache Coherent Multicore Architectures

Authors: Shiji Bijo, Einar Broch Johnsen, Ka I Pun, S. Lizeth Tapia Tarifa

Publication Year: 2016.

Abstract: This paper presents a formal semantics of multicore architectures with private cache, shared memory, and instantaneous inter-core communications. The purpose of the semantics is to provide an operational understanding of how low-level read and write operations interact with caches and main memory. The semantics is based on an abstract model of cache coherence and allows formal reasoning over parallel programs that execute on any given number of cores. We prove correctness properties expressed as invariants for the preservation of program order, data-race free execution of low-level operations, and no access to stale data.


A Maude Framework for Cache Coherent Multicore Architectures

Authors: Shiji Bijo, Einar Broch Johnsen, Ka I Pun, Silvia Lizeth Tapia Tarifa

Publication Year: 2016.

Abstract: On shared memory multicore architectures, cache memory is used to accelerate program execution by providing quick access to recently used data, but enables multiple copies of data to co-exist during execution. Although cache coherence protocols ensure that cores do not access stale data, the organisation of data in memory and the scheduling of tasks may significantly influence the performance of a parallel program in this setting. As a step towards understanding how the data organisation impacts the performance of a given parallel program using shared memory, this paper proposes a framework defined in Maude for the executable modelling of program execution on cache coherent multicore architectures, formalising the interactions between cores executing tasks, their caches, and main memory. The framework allows the specification and comparison of program execution with different design choices for the underlying hardware architecture, such as the number of cores, the data layout in main memory, and the cache associativity.

Vats: A Safe, Reactive Storage Abstraction

Authors: Dave ClarkeTobias Wrigstad

Publication Year: 2016.

Abstract: The rise of multicore computers has hastened the advent of multifarious abstractions to facilitate the construction of parallel programs. This paper presents another: the vat. A vat is like a variable, but it has various actions attached to it that can block, transform and react to changes to the vat. Vats can be combined together in various ways, linking the behaviours of the vats together, resulting in various synchronisation mechanisms. Vats are powerful enough to encode (part of) many existing mechanisms including promises, condition variables, LVars and reactive programming.

 

ParT: An Asynchronous Parallel Abstraction for Speculative Pipeline Computations

Authors: Kiko Fernandez-Reyes, Dave Clarke, and Daniel S. McCain

Publication Year: 2016.

Abstract: The ubiquity of multicore computers has forced programming language designers to rethink how languages express parallelism and concurrency. This has resulted in new language constructs and new combinations or revisions of existing constructs. In this line, we extended the programming languages Encore (actor-based), and Clojure (functional) with an asynchronous parallel abstraction called ParT, a data structure that can dually be seen as a collection of asynchronous values (integrating with futures) or a handle to a parallel computation, plus a collection of combinators for manipulating the data structure. The combinators can express parallel pipelines and speculative parallelism. This paper presents a typed calculus capturing the essence of ParT, abstracting away from details of the Encore and Clojure programming languages. The calculus includes tasks, futures, and combinators similar to those of Orc but implemented in a non-blocking fashion. Furthermore, the calculus strongly mimics how ParT is implemented, and it can serve as the basis for adaptation of ParT into different languages and for further extensions. 

 

Ownership and Reference Counting based Garbage Collection in the Actor World

Authors: Sylvan Clebsch, Sebastian Blessing, Juliana Franco and Sophia Drossopoulou

Publication Year: 2015.

Abstract: We propose Pony-ORCA, a fully concurrent protocol for garbage collection in the actor paradigm. It allows actors to perform garbage collection concurrently with any number of other actors. It does not require any form of synchronization across actors except those introduced through the actor paradigm, i.e. message send and message receive. Pony-ORCA is based on ideas from ownership and deferred, distributed, weighted reference counting. It adapts the messaging system of actors to keep the reference count consistent. We introduce a formal model and describe the invariants on which it relies. We illustrate these invariants through an example and sketch how they are maintained. We show some benchmarks and argue that the protocol can be implemented efficiently.

 

History-Based Specification and Verification of Scalable Concurrent and Distributed Systems

Authors: Crystal Chang Din, S. Lizeth Tapia Tarifa, Reiner Hähnle, Einar Broch Johnsen

Publication Year: 2015.

Abstract: The ABS modelling language targets concurrent and distributed object-oriented systems. The language has been designed to enable scalable formal verification of detailed executable models. This paper provides evidence for that claim: it gives formal specifications of safety properties in terms of histories of observable communication for ABS models as well as formal proofs of those properties. We illustrate our approach with a case study of a Network-on-Chip packet switching platform. We provide an executable formal model in ABS of a generic m×n mesh chip with an unbounded number of packets and verify several crucial properties. Our concern is formal verification of unbounded concurrent systems. In this paper we show how scalable verification can be achieved by compositional and local reasoning about history-based specifications of observable behavior.

 

Refined Ownership: Fine-Grained Controlled Internal Sharing

Authors: Elias Castegren, Johan Ostlund, and Tobias Wrigstad

Publication Year: 2015.

Abstract: Ownership type systems give a strong notion of separation between aggregates. Objects belonging to different owners cannot be aliased, and thus a mutating operation internal to one object is guaranteed to be invisible to another. This naturally facilitates reasoning about correctness on a local scale, but also proves beneficial for coarse-grained parallelism as noninterference between statements touching different objects is easily established. For fine-grained parallelism, ownership types fall short as owner-based disjointness only allows separation of the innards of different aggregates, which is very coarse-grained. Concretely: ownership types can reason about the disjointness of two different data structures, but cannot reason about the internal structure or disjointness within the data structure, without resorting to static and overly constraining measures. For similar reasons, ownership fails to determine internal disjointness of external pointers to objects that share a common owner. In this paper, we introduce the novel notion of refined ownership which overcomes these limitations by allowing precise local reasoning about a group of objects even though they belong to the same external owner. Using refined ownership, we can statically check determinism of parallel operations on tree-shaped substructures of a data structure, including operations on values external to the structure, without imposing any non-local alias restrictions.

 

Parallel Objects for Multicores: A Glimpse at the Parallel Language ENCORE

Authors: Stephan Brandauer, Elias Castegren, Dave Clarke , Kiko Fernandez-Reyes, Einar Broch Johnsen, Ka I. Pun, S. Lizeth Tapia Tarifa, Tobias Wrigstad, and Albert Mingkun Yang

Publication Year: 2015.

Abstract: The age of multi-core computers is upon us, yet current programming languages, typically designed for single-core computers and adapted post hoc for multi-cores, remain tied to the constraints of a sequential mindset and are thus in many ways inadequate. New programming language designs are required that break away from this oldfashioned mindset. To address this need, we have been developing a new programming language called Encore, in the context of the European Project UpScale. The paper presents a motivation for the Encore language, examples of its main constructs, several larger programs, a formalisation of its core, and a discussion of some future directions our work will take. The work is ongoing and we started more or less from scratch. That means that a lot of work has to be done, but also that we need not be tied to decisions made for sequential language designs. Any design decision can be made in favour of good performance and scalability. For this reason, Encore offers an interesting platform for future exploration into object-oriented parallel programming.


From Communicating machines to graphical Choreographies

Authors: Julien Lange, Emilio Tuosto and Nobuko Yoshida

Publication Year: 2015

Abstract: Graphical choreographies, or global graphs, are general multiparty session specifications featuring expressive constructs such as forking, merging, and joining for representing application-level protocols. Global graphs can be directly translated into modelling notations such as BPMN and UML. This paper presents an algorithm whereby a global graph can be constructed from asynchronous interactions represented by communicating finite-state machines (CFSMs). Our results include: a sound and complete characterisation of a subset of safe CFSMs from which global graphs can be constructed; an algorithm to translate CFSMs to global graphs; a time complexity analysis; and an implementation of our theory, as well as an experimental evaluation.

Globally Governed Session Semantics

Authors: Dimitrios Kouzapas and Nobuko Yoshida

Publication Year: 2015

Abstract: This paper proposes a bisimulation theory based on multiparty session types where a choreography specification governs the behaviour of session typed processes and their observer. The bisimulation is defined with the observer cooperating with the observed process in order to form complete global session scenarios and usable for proving correctness of optimisations for globally coordinating threads and processes. The induced bisimulation is strictly more fine-grained than the standard session bisimulation. The difference between the governed and standard bisimulations only appears when more than two interleaved multiparty sessions exist. This distinct feature enables to reason real scenarios in the large-scale distributed system where multiple choreographic sessions need to be interleaved. The compositionality of the governed bisimilarity is proved through the soundness and completeness with respect to the governed reduction-based congruence. Finally, its usage is demonstrated by a thread transformation governed under multiple sessions in a real usecase in the large-scale cyberinfrustracture.



Global Escape in Multiparty Sessions

Authors: Sara Capecchi, Elena Giachino and Nobuko Yoshida

Publication Year: 2015

Abstract: This article proposes a global escape mechanism which can handle unexpected or unwanted conditions changing the default execution of distributed communicational flows, preserving compatibility of the multiparty conversations. Our escape is realised by a collection of asynchronous local exceptions which can be thrown at any stage of the communication and to any subsets of participants in a multiparty session. This flexibility enables to model complex exceptions such as criss-crossing global interactions and error handling for distributed cooperating threads. Guided by multiparty session types, our semantics is proven to provide a termination algorithm for global escapes. Our type system guarantees further safety and liveness properties, such as progress within the session and atomicity of escapes with respect to the subset of involved participants.



Global Progress for Dynamically Interleaved Multiparty Sessions

Authors: Mario Coppo, Mariangiola Dezani-Ciancaglini, Nobuko Yoshida and Luca Padovani

Publication Year: 2015

Abstract: A multiparty session forms a unit of structured communication among many participants which follow communication sequences specified as a global type. When a process is engaged in two or more sessions simultaneously, different sessions can be interleaved and can interfere at runtime. Previous work on multiparty session types has ignored session interleaving, providing a limited progress property ensured only within a single session, by assuming non-interference among different sessions and by forbidding delegation. This paper develops, besides a more traditional, compositional communicationtype system, a novel static interactiontype system for global progress in dynamically interleaved and interfered multiparty sessions. The interaction type system infers causalities of channels making sure that processes do not get stuck at intermediate stages of sessions also in presence of delegation.



On Asynchronous Eventful Session Semantics

Authors: Dimitrios Kouzapas, Nobuko Yoshida, Raymond Hu and Kohei Honda

Publication Year: 2015

Abstract: Event-driven programming is one of the major paradigms in concurrent and communication-based programming, where events are typically detected as the arrival of messages on asynchronous channels. Unfortunately, the flexibility and performance of traditional event-driven programming come at the cost of more complex programs: low-level APIs and the obfuscation of event-driven control flow make programs difficult to read, write and verify. This paper introduces a Ï€-calculus with session types that models event-driven session programming (called ESP) and studies its behavioural theory. The main characteristics of the ESP model are asynchronous, order-preserving message passing, non-blocking detection of event/message arrivals and dynamic inspection of session types. Session types offer formal safety guarantees, such as communication and event handling safety, and programmatic benefits that overcome problems with existing event-driven programming languages and techniques. The new typed bisimulation theory developed for the ESP model is distinct from standard synchronous or asynchronous bisimulation, capturing the semantic nature of eventful session-based processes. The bisimilarity coincides with reduction-closed barbed congruence. We demonstrate the features and benefits of ESP and the behavioural theory through two key use cases. First, we examine an encoding and the semantic behaviour of the event selector, a central component of general event-driven systems, providing core results for verifying type-safe event-driven applications. Second, we examine the Lauer“Needham duality, building on the selector encoding and bisimulation theory to prove that a systematic transformation from multithreaded to event-driven session processes is type- and semantics-preserving.



Practical interruptible conversations Distributed dynamic verification with multiparty session types and Python

Authors: Romain Demangeon, Kohei Honda, Raymond Hu, Rumyana Neykova and Nobuko Yoshida

Publication Year: 2015

Abstract: The rigorous and comprehensive verification of communication-based software is an important engineering challenge in distributed systems. Drawn from our industrial collaborations [40,34] on Scribble, a choreography description language based on multiparty session types, and its theoretical foundations [20], this article proposes a dynamic verification framework for structured interruptible conversation programming. We first present our extension of Scribble to support the specification of asynchronously interruptible conversations. We then implement a concise API for conversation programming with interrupts in Python that enables session types properties to be dynamically verified for distributed processes. Finally, we expose the underlying theory of our interrupt mechanism, studying its syntax and semantics, its integration in MPST theory and proving the correctness of our design. Our framework ensures the global safety of a system in the presence of asynchronous interrupts through independent runtime monitoring of each endpoint, checking the conformance of the local execution trace to the specified protocol. The usability of our framework for describing and verifying choreographic communications has been tested by integration into the large scientific cyberinfrastructure developed by the Ocean Observatories Initiative. Asynchronous interrupts have proven expressive enough to represent and verify their main classes of communication patterns, including asynchronous streaming and various timeoutbased protocols, without introducing any implicit synchronisations. Benchmarks show conversation programming and monitoring can be realised with little overhead.

High Performance Computing Applications using Parallel Data Processing Units

Authors: Keyvan Azadbakht, Vlad Serbanescu, and Frank de Boer

Publication Year: 2015

Abstract: Multicore processors are growing with respect to the number of cores on a chip. In a parallel computation context, multicore platforms have several important features such as exploiting multiple parallel processes, having access to a shared memory with noticeably lower cost than the distributed alternative and optimizing different levels of parallelism. In this paper, we introduce the Parallel Data Processing Unit (PDPU) which is a group of objects that benefits from the shared memory of the multicore configuration and that consists of two parts: a shared memory for maintaining data consistent, and a set of objects that are processing the data, then producing and aggregating the results concurrently. We then implement two examples in Java that illustrate PDPU behavior, and compare them with their actor based counterparts and show significant performance improvements. We also put forward the idea of integrating PDPU with the actor model which will result in an optimization for a specific spectrum of problems in actor based development.

Towards Type Based Optimizations in Distributed Applications using ABS and Java 8

Authors: Vlad Serbanescu, Chetan Nagarajagowda, Keyvan Azadbakht, Frank de Boer and Behrooz Nobakht.

Publication Year: 2014.

Abstract: In this paper we present an API to support modeling applications with Actors based on the paradigm of the Abstract Behavioural Specification (ABS) language. With the introduction of JAVA 8, we expose this API through a JAVA library to allow for a high-level actor-based methodology for programming distributed systems which supports the programming to interfaces discipline. We validate this solution through a case study where we obtain significant performance improvements as well as illustrating the ease with which simple high and low-level optimizations can be obtained by examining topologies and communication within an application. Using this API we show it is much easier to observe drawbacks of shared data-structures and communications methods in the design phase of a distributed application and apply the necessary corrections in order to obtain better results.

Scaling Future Software : The Manycore Challenge

Authors: Frank de Boer, Einar Broch Johnsen, Dave Clarke, Sophia Drossopoulou, Nobuko Yoshida and Tobias Wrigstad.

Publication Year : 2014.

Abstract: Existing software cannot benefit from the revolutionary potential increases in computational power provided by manycore chips unless their design and code are polluted by an unprecedented amount of low-level, fine-grained concurrency detail. As a consequence, the advent of manycore chips threatens to make current main-stream programming approaches obsolete, and thereby, jeopardizes the benefits gained from the last 20 years of development in industrial software engineering. In this article we put forward an argument for a fundamental breakthrough in how parallelism and concurrency are integrated into the software of the future.



A formal model of service-oriented dynamic object groups

Authors : Einar Broch Johnsen, Olaf Owe, Dave Clarke and Joakim Bjork.

Publication Year : 2014

Abstract: Services are autonomous, self-describing, technology-neutral software units that can be published, discovered, queried, and composed into software applications at runtime. Designing and composing software services to form applications or composite services, require abstractions beyond those found in typical object-oriented programming languages. This paper explores service-oriented abstractions such as service adaptation, discovery, and querying in an object-oriented setting. We develop a formal model of dynamic object-oriented groups which offer services to their environment. These groups fit directly into the object-oriented paradigm in the sense that they can be dynamically created, they have an identity, and they can receive method calls. In contrast to objects, groups are not used for structuring code. A group exports its services through interfaces and relies on objects to implement these services. Objects may join or leave different groups. Groups may dynamically export new interfaces, they support service discovery, and they can be queried at runtime for the interfaces they support. We define an operational semantics and a static type system for this model of dynamic object groups, and show that well-typed programs do not cause method-not-understood errors at runtime.



Behavioral types for non-uniform memory accesses.

Authors: Juliana Franco and Sophia Drossopoulou

Publication Year: 2014

Abstract: Concurrent programs executing on NUMA architectures consist of concurrent entities (e.g. threads, actors) and data placed on different nodes. Execution of these concurrent entities often reads or updates state from remote nodes. The performance of such systems depends on the extent to which the concurrent entities can be executing in parallel, and on the amount of the remote reads and writes. We consider an actor-based object oriented language, and propose a type system which expresses the topology of the program (the placement of the actors and data on the nodes), and an effect system which characterises remote reads and writes (in terms of which node reads/writes from which other nodes). We use a variant of ownership types for the topology, and a combination of behavioural and ownership types for the effect system.



Calculating communication costs with Sessions Types and Sizes.

Authors:Juliana Franco, Sophia Drossopoulou, and Nobuko Yoshida

Publication Year:2014

Abstract: We present a small object-oriented language with communication primitives. The language allows the assignment of binary session types to communication channels in order to govern the interaction between different objects and to statically calculate communication costs. Class declarations are annotated with size information in order to determine the cost of sending and receiving objects. This paper describes our first steps in the creation of a session-based, object-oriented language for communication optimization purposes.



Capable: Capabilities for Scalability

Authors: Elias Castegren and Tobias Wrigstad

Abstract: This paper describes the current state of the design of the Capable system, which explores the use of capability-based alias management for parallel programming. Capable allows aliasing as long as all aliases offer non-conflicting capabilities to possibly shared resources, thereby avoiding the need to propagate effect information and opening up for flexible programming which is generally not possible with effect systems. Classes are formed from combinations of capabilities, and combinators influence object layout to avoid false sharing. This allows reusing a single declaration in both memory-efficient and parallel-efficient ways. Finally, Capable capabilities supports patterns of lock-free programming with the goal of providing a limited form of static checking for typical lock-free idioms.



Pabble: Parameterised Scribble

Authors: Nicholas Ng, and Nobuko Yoshida

Publication Year: 2014

Abstract: Many parallel and distributed message-passing programs are written in a parametric way over available resources, in particular the number of nodes and their topologies, so that a single parallel program can scale over different environments. This article presents a parameterised protocol description language, Pabble, which can guarantee safety and progress in a large class of practical, complex parameterised message-passing programs through static checking. Pabble can describe an overall interaction topology, using a concise and expressive notation, designed for a variable number of participants arranged in multiple dimensions. These parameterised protocols in turn automatically generate local protocols for type checking parameterised MPI programs for communication safety and deadlock freedom. In spite of undecidability of endpoint projection and type checking in the underlying parameterised session type theory, our method guarantees the termination of end point projection and type checking.



Multiparty Session Nets

Authors: Luca Fossati, Raymond Hu, and Nobuko Yoshida

Publication Year: 2014

Abstract: This paper introduces global session nets, an integration of multiparty session types (MPST) and Petri nets, for role-based choreographic specifications to verify distributed multiparty systems. The graphical representation of session nets enables more liberal combinations of branch, merge, fork and join patterns than the standard syntactic MPST. We use session net token dynamics to verify a flexible conformance between the graphical global net and syntactic endpoint types, and apply the conformance to ensure type-safety and progress of endpoint processes with channel mobility. We have implemented Java APIs for validating global session graph well-formedness and endpoint type conformance.



Rationally Reconstructing the Escrow Example

Authors: James Noble and Sophia Drossopoulou

Publication Year: 2014.

Abstract: The Escrow Exchange Contract has been used as a case study of building up complex and trustworthy systems from basic object capabilities, in the context of concurrent and distributed programming. In this short paper we present a Rational Reconstruction of the Escrow Exchange Contract case study, expressed in Grace, concentrating on the most essential issues of trustworthiness, and ignoring issues to do with distribution or more complex protocols. We then use our notation for capability policies to specify the key features of the reconstructed case study.

 

How to Break the Bank: Semantics of Capability Policies

Authors: Sophia Drossopoulou and James Noble

Publication Year: 2014

Abstract: The object capability model is a de-facto industry standard widely adopted for the implementation of secure software. We call capability policies the policies enforced by programs using object capabilities. Such policies tend to restrict the objects and the circumstances which may access services. In this paper we argue that capability policies should be made explicit and written separately from the code implementing them. We also argue that the specification of capability policies requires concepts that go beyond the features of current specification languages. Moreover, we argue that we need methodologies with which to prove that programs adhere to their capability policies as specified. To give precise semantics to capability policy specifications, we propose execution observations, which talk about various properties of a program™s execution. We use execution observations to write the formal specification of five out of the six informal policies in the mint example, famous in the object capability literature. In these specifications, the conclusions but also the premises may relate to the state before as well as after execution, the code may be existentially or universally quantified, and interpretation quantifies over all modules extending the current module. In statically typed languages, adherence of code to the capability policies relies heavily on the guarantees provided by type system features such as final and private.