178 results found
Boer F, Einar Broch J, Clarke D, et al., Scaling Future Software: The Manycore Challenge, ERCIM News, Vol: 2014
Chen T-C, Dezani-Ciancaglini M, Scalas A, et al., On the preciseness of subtyping in session types, Logical Methods in Computer Science, ISSN: 1860-5974
Subtyping in concurrency has been extensively studied since early 1990s asone of the most interesting issues in type theory. The correctness of subtyping relations hasbeen usually provided as the soundness for type safety. The converse direction, the com-pleteness, has been largely ignored in spite of its usefulness to de ne the largest subtypingrelation ensuring type safety. This paper formalises preciseness (i.e. both soundness andcompleteness) of subtyping for mobile processes and studies it for the synchronous and theasynchronous session calculi. We rst prove that the well-known session subtyping, thebranching-selection subtyping, is sound and complete for the synchronous calculus. Nextwe show that in the asynchronous calculus, this subtyping is incomplete for type-safety:that is, there exist session typesTandSsuch thatTcan safely be considered as a subtypeofS, butT6Sis not derivable by the subtyping. We then propose an asynchronous sub-typing system which is sound and complete for the asynchronous calculus. The methodgives a general guidance to design rigorous channel-based subtypings respecting desiredsafety properties. Both the synchronous and the asynchronous calculus are rst consid-ered with linear channels only, and then they are extended with session initialisations andcommunications of expressions (including shared channels).
Imai K, Yoshida N, Yuen S, Session-ocaml: a session-based library with polarities and lenses, 19th International Conference on Coordination Models and Languages
Neykova R, Bocchi L, Yoshida N, Timed Runtime Monitoring for Multiparty Conversations, Electronic Proceedings in Theoretical Computer Science, EPTCS, ISSN: 2075-2180
Neykova R, Yoshida N, Multiparty session actors, Logical Methods in Computer Science, ISSN: 1860-5974
Actor coordination armoured with a suitable protocol description language has beena 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 introduc-ing minimum additions to the model such as the notion of actor roles and protocol mailboxes. Theframework uses Scribble, which is a protocol description language based on multiparty session types.Our programming model supports actor-like syntax and runtime verification mechanism guarantee-ing communication safety of the participating entities. An actor can implement multiple roles in asimilar way as an object can implement multiple interfaces. Multiple roles allow for cooperativeinter-concurrency in a single actor. We demonstrate our framework by designing and implement-ing a session actor library in Python and its runtime verification mechanism. Benchmark resultsdemonstrate that the runtime checks induce negligible overhead. We evaluate the applicability of ourverification framework to specify actor interactions by implementing twelve examples from an actorbenchmark suit.
Orchard D, Rice A, Oshmyan O, Evolving Fortran types with inferred units-of-measure, Journal of Computational Science, ISSN: 1877-7503
Pérez JA, Kouzapas D, Yoshida N, Core Higher-Order Session Processes: Tractable Equivalences and Relative Expressiveness, Logic in Computer Science
Scalas A, Dardha O, Hu R, et al., A Linear Decomposition of Multiparty Sessions for Safe Distributed Programming, 31st European Conference on Object-Oriented Programming (ECOOP 2017)
Bocchi L, Chen T-C, Demangeon R, et al., 2017, Monitoring networks through multiparty session types, THEORETICAL COMPUTER SCIENCE, Vol: 669, Pages: 33-58, ISSN: 0304-3975
Graversen E, Phillips I, Yoshida N, 2017, Towards a categorical representation of reversible event structures, Pages: 49-60, ISSN: 2075-2180
© E. Graversen, I. Phillips, & N. Yoshida.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.
Hu R, Yoshida N, 2017, Explicit connection actions in multiparty session types, Pages: 116-133, ISSN: 0302-9743
© Springer-Verlag GmbH Germany 2017.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.
Kouzapas D, Perez JA, Yoshida N, 2017, Characteristic bisimulation for higher-order session processes, ACTA INFORMATICA, Vol: 54, Pages: 271-341, ISSN: 0001-5903
Lange J, Ng N, Toninho B, et al., 2017, Fencing off Go: Liveness and Safety for Channel-Based Programming, Publisher: ASSOC COMPUTING MACHINERY, Pages: 748-761, ISSN: 0362-1340
Lange J, Yoshida N, 2017, On the undecidability of asynchronous session subtyping, Pages: 441-457, ISSN: 0302-9743
© Springer-Verlag GmbH Germany 2017.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 sub-class 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.
Neykova R, Bocchi L, Yoshida N, 2017, Timed runtime monitoring for multiparty conversations, Formal Aspects of Computing, Pages: 1-34, ISSN: 0934-5043
© 2017 The Author(s)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.
Neykova R, Yoshida N, 2017, Let it recover: Multiparty protocol-induced recovery, Pages: 98-108
© 2017 ACM.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.
Scalas A, Yoshida N, 2017, Multiparty session types, beyond duality (Abstract), Pages: 37-38, ISSN: 2075-2180
© A. Scalas and N. Yoshida.Multiparty Session Types (MPST) are a well-established typing discipline for message-passing processes interacting on sessions involving two or more participants. Session typing can ensure desirable properties: absence of communication errors and deadlocks, and protocol conformance. However, existing MPST works provide a subject reduction result that is arguably (and sometimes, surprisingly) restrictive: it only holds for typing contexts with strong duality constraints on the interactions between pairs of participants. Consequently, many "intuitively correct" examples cannot be typed and/or cannot be proved type-safe. We illustrate some of these examples, and discuss the reason for these limitations. Then, we outline a novel MPST typing system that removes these restrictions.
Debois S, Hildebrandt T, Slaats T, et al., 2016, TYPE-CHECKING LIVENESS FOR COLLABORATIVE PROCESSES WITH BOUNDED AND UNBOUNDED RECURSION, LOGICAL METHODS IN COMPUTER SCIENCE, Vol: 12, ISSN: 1860-5974
Debois S, Hildebrandt T, Slaats T, et al., 2016, Type-checking liveness for collaborative processes with bounded and unbounded recursion, Logical Methods in Computer Science, Vol: 12
© S. Debois, T. Hildebrandt, T. Slaats, and N. Yoshida.We present the first session typing system guaranteeing request-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 (databased) 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.
Dezani-Ciancaglini M, Ghilezan S, Jakšić S, et al., 2016, Denotational and operational preciseness of subtyping: A roadmap, Pages: 155-172, ISBN: 9783319307336
© Springer International Publishing Switzerland 2016.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.
Dezani-Ciancaglini M, Ghilezan S, Jakšić S, et al., 2016, Precise subtyping for synchronous multiparty sessions, Electronic Proceedings in Theoretical Computer Science, EPTCS, Vol: 203, Pages: 29-43, ISSN: 2075-2180
© Dezani, Ghilezan, Jakšić, Pantović, Yoshida.The notion of subtyping has gained an important role both in theoretical and applicative domains: in lambda and concurrent calculi as well as in programming languages. The soundness and the completeness, together referred to as the preciseness of subtyping, can be considered from two different points of view: operational and denotational. The former 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 latter preciseness is based on the denotation of a type which is a mathematical object that describes the meaning of the type in accordance with the denotations of other expressions from the language. The result of this paper is the operational and denotational preciseness of the subtyping for a synchronous multiparty session calculus. The novelty of this paper is the introduction of characteristic global types to prove the operational completeness.
Honda K, Yoshida N, Carbone M, 2016, Multiparty Asynchronous Session Types, JOURNAL OF THE ACM, Vol: 63, ISSN: 0004-5411
Hu R, Yoshida N, 2016, Hybrid Session Verification Through Endpoint API Generation, 19th International Conference on Fundamental Approaches to Software Engineering (FASE) held as part of Annual European Joint Conferences on Theory and Practice of Software (ETAPS), Publisher: SPRINGER-VERLAG BERLIN, Pages: 401-418, ISSN: 0302-9743
Kouzapas D, Pérez JA, Yoshida N, 2016, On the relative expressiveness of higher-order session processes, Pages: 446-475, ISSN: 0302-9743
© Springer-Verlag Berlin Heidelberg 2016.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 equivalence) more precisely and efficiently than the first-order session π-calculus (π). Overall, under session types, HOπ, HO, and π are equally expressive; however, HOπ and HO are more tightly related than HOπ and π.
Lange J, Yoshida N, 2016, Characteristic formulae for session types, Pages: 833-850, ISSN: 0302-9743
© Springer-Verlag Berlin Heidelberg 2016.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.
Mycroft A, Orchard DA, Petricek T, 2016, Effect Systems Revisited - Control-Flow Algebra and Semantics., Semantics, Logics, and Calculi - Essays Dedicated to Hanne Riis Nielson and Flemming Nielson on the Occasion of Their 60th Birthdays, Editors: Probst, Hankin, Hansen, Publisher: Springer, Pages: 1-32, ISBN: 978-3-319-27809-4
Ng N, Yoshida N, 2016, Static Deadlock Detection for Concurrent Go by Global Session Graph Synthesis, 25th International Conference on Compiler Construction (CC), Publisher: ASSOC COMPUTING MACHINERY, Pages: 174-184
Niu X, Ng N, Yuki T, et al., 2016, EURECA Compilation: Automatic Optimisation of Cycle-Reconfigurable Circuits, 26th International Conference on Field-Programmable Logic and Applications (FPL), Publisher: IEEE, ISSN: 1946-1488
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.