Publications
373 results found
Demangeon R, Honda K, Hu R, et al., 2014, Practical interruptible conversations: distributed dynamic verification with multiparty session types and Python, Formal Methods in System Design, Vol: 46, Pages: 197-225, ISSN: 1572-8102
The rigorous and comprehensive verification of communication-based software is an important engineering challenge in distributed systems. Drawn from our industrial collaborations (Ocean Observatories Initative, http://www.oceanobservatories.org/, JBoss Savara Project, http://www.jboss.org/savara) on Scribble, a choreography description language based on multiparty session types, and its theoretical foundations (Honda et al., in POPL, pp 273–284, 2008), 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 timeout-based protocols, without introducing any implicit synchronisations. Benchmarks show conversation programming and monitoring can be realised with little overhead.
Capecchi S, Giachino E, Yoshida N, 2014, Global escape in multiparty sessions, Mathematical Structures in Computer Science, Vol: 29, ISSN: 1469-8072
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 realized 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.
Kouzapas D, Yoshida N, Hu R, et al., 2014, On asynchronous eventful session semantics, Mathematical Structures in Computer Science, Vol: 29, ISSN: 0960-1295
© Cambridge University Press 2014. 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.
Soares Cogumbreiro Garcia T, Hu R, Martins F, et al., 2014, Dynamic deadlock verification for general barrier synchronisation, 20th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming (PPoPP 2015)
We present Armus, a dynamic verification tool for deadlock detection and avoidance specialised in barrier synchronisation. Barriers are used to coordinate the execution of groups of tasks, and serve as a building block of parallel computing. Our tool verifies more barrier synchronisation patterns than current state-of-the-art. To improve the scalability of verification, we introduce a novel event-based representation of concurrency constraints, and a graph-based technique for deadlock analysis. The implementation is distributed and fault-tolerant, and can verify X10 and Java programs. To formalise the notion of barrier deadlock, we introduce a core language expressive enough to represent the three most widespread barrier synchronisation patterns: group, split-phase, and dynamic membership. We propose a graph analysis technique that selects from two alternative graph representations: the Wait-For Graph, that favours programs with more tasks than barriers; and the State Graph, optimised for programs with more barriers than tasks. We prove that finding a deadlock in either representation is equivalent, and that the verification algorithm is sound and complete with respect to the notion of deadlock in our core language. Armus is evaluated with three benchmark suites in local and distributed scenarios. The benchmarks show that graph analysis with automatic graph-representation selection can record a 7-fold execution increase versus the traditional fixed graph representation. The performance measurements for distributed deadlock detection between 64 processes show negligible overheads.
Coppo M, Dezani-Ciancaglini M, Yoshida N, et al., 2014, Global progress for dynamically interleaved multiparty sessions, Mathematical Structures in Computer Science, Vol: 760, ISSN: 1469-8072
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 communication type system, a novel static interaction type 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.
Boer F, Einar Broch J, Clarke D, et al., 2014, Scaling Future Software: The Manycore Challenge, ERCIM News, Vol: 2014
Chen T-C, Dezani-Ciancaglini M, Yoshida N, 2014, On the Preciseness of Subtyping in Session Types, Principles and Practice of Declarative Programming (PPDP'14), Publisher: ACM, Pages: 135-146
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 greatest 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 this fact 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.
Franco J, Drossopoulou S, Yoshida N, 2014, Calculating communication costs with Sessions Types and Sizes, Pages: 50-57, ISSN: 2190-6807
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.
Neykova R, Bocchi L, Yoshida N, 2014, Timed Runtime Monitoring for Multiparty Conversations, Electronic Proceedings in Theoretical Computer Science, EPTCS, ISSN: 2075-2180
Neykova R, Bocchi L, Yoshida N, 2014, Timed Runtime Monitoring for Multiparty Conversations, Electronic Proceedings in Theoretical Computer Science, Vol: 162, Pages: 19-26, ISSN: 2075-2180
Honda K, Yoshida N, Berger M, 2014, Process types as a descriptive tool for interaction control and the Pi-calculus, Joint International Conference, RTA-TLCA 2014, Publisher: Springer, Pages: 1-20, ISSN: 0302-9743
We demonstrate a tight relationship between linearly typed π-calculi and typed λ-calculi by giving a type-preserving translation from the call-by-value λμ-calculus into a typed π-calculus. The λμ-calculus has a particularly simple representation as typed mobile processes. The target calculus is a simple variant of the linear π-calculus. We establish full abstraction up to maximally consistent observational congruences in source and target calculi using techniques from games semantics and process calculi. © 2014 Springer International Publishing Switzerland.
Tiezzi F, Yoshida N, 2014, Towards reversible sessions, Electronic Proceedings in Theoretical Computer Science, EPTCS, Vol: 155, Pages: 17-24, ISSN: 2075-2180
In this work, we incorporate reversibility into structured communication-based programming, to allow parties of a session to automatically undo, in a rollback fashion, the effect of previously executed interactions. This permits taking different computation paths along the same session, as well as reverting the whole session and starting a new one. Our aim is to define a theoretical basis for examining the interplay in concurrent systems between reversible computation and session-based interaction. We thus enrich a session-based variant of π-calculus with memory devices, dedicated to keep track of the computation history of sessions in order to reverse it. We discuss our initial investigation concerning the definition of a session type discipline for the proposed reversible calculus, and its practical advantages for static verification of safe composition in communication-centric distributed software performing reversible computations.
Honda K, Yoshida N, Berger M, 2014, An observationally complete program logic for imperative higher-order functions, THEORETICAL COMPUTER SCIENCE, Vol: 517, Pages: 75-101, ISSN: 0304-3975
Bocchi L, Yang W, Yoshida N, 2014, Timed multiparty session types, Pages: 419-434, ISSN: 0302-9743
We propose a typing theory, based on multiparty session types, for modular verification of real-time choreographic interactions. To model real-time implementations, we introduce a simple calculus with delays and a decidable static proof system. The proof system ensures type safety and time-error freedom, namely processes respect the prescribed timing and causalities between interactions. A decidable condition on timed global types guarantees time-progress for validated processes with delays, and gives a sound and complete characterisation of a new class of CTAs with general topologies that enjoys progress and liveness. © 2014 Springer-Verlag.
Cogumbreiro T, Hu R, Martins F, et al., 2014, Dynamic deadlock verification for general barrier synchronisation, Departmental Technical Report: 14/12, Publisher: Department of Computing, Imperial College London, 14/12
We present Armus, a dynamic verification tool for deadlock detectionand avoidance specialised in barrier synchronisation. Barriersare used to coordinate the execution of groups of tasks, and serve asa building block of parallel computing. Our tool verifies more barriersynchronisation patterns than current state-of-the-art. To improvethe scalability of verification, we introduce a novel eventbasedrepresentation of concurrency constraints, and a graph-basedtechnique for deadlock analysis. The implementation is distributedand fault-tolerant, and can verify X10 and Java programs.To formalise the notion of barrier deadlock, we introduce a corelanguage expressive enough to represent the three most widespreadbarrier synchronisation patterns: group, split-phase, and dynamicmembership. We propose a graph analysis technique that selectsfrom two alternative graph representations: the Wait-For Graph,that favours programs with more tasks than barriers; and the StateGraph, optimised for programs with more barriers than tasks. Weprove that finding a deadlock in either representation is equivalent,and that the verification algorithm is sound and complete withrespect to the notion of deadlock in our core language.Armus is evaluated with three benchmark suites in local anddistributed scenarios. The benchmarks show that graph analysiswith automatic graph-representation selection can record a 7-foldexecution increase versus the traditional fixed graph representation.The performance measurements for distributed deadlock detectionbetween 64 processes show negligible overheads.
Fossati L, Hu R, Yoshida N, 2014, Multiparty session nets, Departmental Technical Report: 14/5, Publisher: Department of Computing, Imperial College London, 14/5
This paper introduces global session nets, an integration of multipartysession types (MPST) and Petri nets, for role-based choreographicspecifications to verify distributed multiparty systems. The graphical representationof session nets enables more liberal combinations of branch, merge, forkand join patterns than the standard syntactic MPST. We use session net tokendynamics to verify a flexible conformance between the graphical global net andsyntactic endpoint types, and apply the conformance to ensure type-safety andprogress of endpoint processes with channel mobility. We have implementedJava APIs for validating global session graph well-formedness and endpointtype conformance.
Yoshida N, Hu R, Neykova R, et al., 2014, The scribble protocol language, Pages: 22-41, ISSN: 0302-9743
This paper describes a brief history of how Kohei Honda initiated the Scribble project, and summarises the current status of Scribble. © Springer International Publishing Switzerland 2014.
Lange J, Yoshida N, Tuosto E, 2014, Synthesis of graphical choreographies, Departmental Technical Report: 14/4, Publisher: Department of Computing, Imperial College London, 14/4
Graphical choreographies, or global graphs, are general multiparty sessionspecifications featuring expressive constructs such as forking, merging, andjoining for representing application-level protocols. Global graphs can be directlytranslated into modelling notations such as BPMN and UML. This paper presents analgorithm whereby a global graph can be synthesised from asynchronous bufferedbehaviours represented by communicating finite state machines (CFSMs). Our resultsinclude: a sound and complete characterisation of a subset of safe CFSMs fromwhich global graphs can be synthesised; a synthesis algorithm to translate CFSMsto global graphs; a time complexity analysis; and an implementation of our theory,as well as an experimental evaluation.
Bocchi L, Yang W, Yoshida N, 2014, Timed multiparty session types, Departmental Technical Report: 14/3, Publisher: Department of Computing, Imperial College London, 14/3
We propose a typing theory, based on multiparty session types, for modularverification of real-time choreographic interactions. To model real-time implementations,we introduce a simple calculus with delays and a decidable static proof system.The proof system with time constraints ensures type safety and time-error freedom,namely processes respect the prescribed timing and causalities between interactions. Adecidable condition, enforceable on timed global types, guarantees global time-progressfor validated processes with delays, and gives a sound and complete characterisation ofa new class of CTAs with general topologies that enjoys global progress and liveness.
Honda K, Yoshida N, Berger M, 2014, Control in the π-calculus, Departmental Technical Report: 14/2, Publisher: Department of Computing, Imperial College London, 14/2
This paper presents a type-preserving translation from the call-by-value -calculus ( v-calculus) into a typed -calculus, and shows full abstraction up tomaximally consistent observational congruences in both calculi. The -calculushas a particularly simple representation as typed mobile processes where a uniquestateless replicated input is associated to each name. The corresponding -calculusis a proper subset of the linear -calculus, the latter being able to embed the simplytyped -calculus fully abstractly. Strong normalisability of the v-calculus is animmediate consequence of this correspondence and the strong normalisability of thelinear -calculus, using the standard argument based on simulation between the v-calculus and its translation. Full abstraction, our main result, is proved via aninverse transformation from the typed -terms which inhabit the encoded v-typesinto the v-calculus (the so-called de nability argument), using proof techniquesfrom games semantics and process calculi. A tight operational correspondence assistedby the de nability result opens a possibility to use typed -calculi as a toolto investigate and analyse behaviours of various control operators and associatedcalculi in a uniform setting, possibly integrated with other language primitives andoperational structures.
Orrego PR, Olivares H, Cordero EM, et al., 2014, A Cytoplasmic New Catalytic Subunit of Calcineurin in <i>Trypanosoma cruzi</i> and Its Molecular and Functional Characterization, PLOS NEGLECTED TROPICAL DISEASES, Vol: 8, ISSN: 1935-2735
- Author Web Link
- Cite
- Citations: 12
Ng N, Yoshida N, 2014, Pabble: Parameterised Scribble for Parallel Programming
Honda K, Hu R, Neykova R, et al., 2014, Structuring Communication with Session Types, International Symposium on Concurrent Objects and Beyond - From Theory to High-Performance Computing, Publisher: SPRINGER-VERLAG BERLIN, Pages: 105-127, ISSN: 0302-9743
- Author Web Link
- Cite
- Citations: 12
Neykova R, Yoshida N, 2014, Multiparty Session Actors, 16th IFIP WG 6.1 International Conference on Coordination Models and Languages (COORDINATION), Publisher: SPRINGER-VERLAG BERLIN, Pages: 131-146, ISSN: 0302-9743
- Author Web Link
- Cite
- Citations: 22
Debois S, Hildebrandt T, Slaats T, et al., 2014, Type Checking Liveness for Collaborative Processes with Bounded and Unbounded Recursion, 34th IFIP WG 6.1 International Conference on Formal Techniques for Distributed Objects, Components and Systems (FORTE), Publisher: SPRINGER-VERLAG BERLIN, Pages: 1-16, ISSN: 0302-9743
- Author Web Link
- Cite
- Citations: 4
Neykova R, Yoshida N, 2014, Multiparty Session Actors, Lecture Notes in Computer Science, Publisher: Springer Berlin Heidelberg, Pages: 131-146, ISBN: 9783662433751
Zanforlin T, Bayer-Santos E, Cortez C, et al., 2013, Molecular Characterization of <i>Trypanosoma cruzi</i> SAP Proteins with Host-Cell Lysosome Exocytosis-Inducing Activity Required for Parasite Invasion, PLOS ONE, Vol: 8, ISSN: 1932-6203
- Author Web Link
- Cite
- Citations: 10
Kouzapas D, Yoshida N, 2013, Globally governed session semantics, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Vol: 8052 LNCS, Pages: 395-409, ISSN: 0302-9743
This paper proposes a new 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. The compositionality of the governed bisimilarity is proved through the soundness and completeness with respect to the governed reduction-based congruence. © 2013 Springer-Verlag.
Montesi F, Yoshida N, 2013, Compositional choreographies, Pages: 425-439, ISSN: 0302-9743
We propose a new programming model that supports a compositionality of choreographies. The key of our approach is the introduction of partial choreographies, which can mix global descriptions with communications among external peers. We prove that if two choreographies are composable, then the endpoints independently generated from each choreography are also composable, preserving their typability and deadlock-freedom. The usability of our framework is demonstrated by modelling an industrial use case implemented in a tool for Web Services, Jolie. © 2013 Springer-Verlag.
Bayer-Santos E, Aguilar-Bonavides C, Rodrigues SP, et al., 2013, Proteomic Analysis of <i>Trypanosoma cruzi</i> Secretome: Characterization of Two Populations of Extracellular Vesicles and Soluble Proteins, JOURNAL OF PROTEOME RESEARCH, Vol: 12, Pages: 883-897, ISSN: 1535-3893
- Author Web Link
- Cite
- Citations: 188
This data is extracted from the Web of Science and reproduced under a licence from Thomson Reuters. You may not copy or re-distribute this data in whole or in part without the written consent of the Science business of Thomson Reuters.