Publications
373 results found
Neykova R, Yoshida N, 2016, Let it recover: multiparty protocol-induced recovery, Departmental Technical Report: 16/10, Publisher: Department of Computing, Imperial College London, 16/10
Fault-tolerant communication systems rely on recovery strategieswhich are often error-prone (e.g. a programmer manually specifiesrecovery strategies) or inefficient (e.g. the whole system is restartedfrom the beginning). This paper proposes a static analysis based onmultiparty session types that can efficiently compute a safe globalstate 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 dependenciesbetween processes and to localise failures. We formalise our recoveryalgorithm and prove its safety. A recovered communicationsystem is free from deadlocks, orphan messages and reception errors.Our recovery algorithm incurs less communication cost (onlyaffected processes are notified) and overall execution time (onlyrequired states are repeated). On top of our analysis, we designand implement a runtime framework in Erlang where failed processesand their dependencies are soundly restarted from a computedsafe state. We evaluate our recovery framework on messagepassingbenchmarks and a use case for crawling webpages. Theexperimental results indicate our framework outperforms a built-instatic recovery strategy in Erlang when a part of the protocol canbe safely recovered.
Lange J, Yoshida N, 2016, On the undecidability of asynchronous session subtyping, Departmental Technical Report: 16/9, Publisher: Department of Computing, Imperial College London, 16/9
Asynchronous session subtyping has been studied extensivelyin [9, 10, 29{32] and applied in [24, 33, 34, 36]. An open question waswhether this subtyping relation is decidable. This paper settles the questionin the negative. To prove this result, we rst introduce a new subclassof two-party communicating nite-state machines (CFSMs), calledasynchronous duplex (ADs), which we show to be Turing complete. Secondly,we give a compatibility relation over CFSMs, which is sound andcomplete wrt. safety for ADs, and is equivalent to the asynchronoussubtyping. Then we show that the halting problem reduces to checkingwhether two CFSMs are in the relation. In addition, we show thecompatibility relation to be decidable for three sub-classes of ADs.
Toninho B, Yoshida N, 2016, Interconnection networks in session-based logical processes, Departmental Technical Report: 16/5, Publisher: Department of Computing, Imperial College London, 16/5
In multiparty session types, interconnection networks identifywhich roles in a session engage in direct communication. If rolep is connected to role q, then p exchanges a message with q.In a session-based interpretation of classical linear logic (CLL),this corresponds to the composition, or cut, of dual propositions.This paper shows that well-formed interactions represented in asession-based interpretation of CLL form strictly less expressiveinterconnection networks than those specified in a multiparty sessioncalculus. To achieve this, we introduce a new compositionalsynthesis property, dubbed partial multiparty compatibility (PMC),enabling us to build a global type denoting the interactions obtainedby iterated composition of well-typed CLL processes.We show thatthe CLL composition rule induces PMC global types without circularinterconnections between three participants. PMC is then usedto define a new CLL multicut rule which can form general multipartyinterconnections, preserving the deadlock-freedom propertyof CLL.
Perera R, Lange J, Gay SJ, 2016, Multiparty Compatibility for Concurrent Objects, 9th Workshop on Programming Language Approaches to Concurrency- and Communication-cEntric Software (PLACES), Publisher: OPEN PUBL ASSOC, Pages: 73-82, ISSN: 2075-2180
- Author Web Link
- Cite
- Citations: 5
Kouzapas D, Yoshida N, Perez J, 2015, Characteristic bisimulation for higher-order session processes, 26th International Conference on Concurrency Theory (CONCUR 2015), Publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik GmbH, Pages: 398-411, ISSN: 1868-8969
Characterising contextual equivalence is a long-standing issue for higher-order (process) languages. In the setting of a higher-order pi-calculus with sessions, 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.
Mycroft A, Orchard D, Petricek T, 2015, Effect Systems Revisited—Control-Flow Algebra and Semantics, Semantics, Logics, and Calculi
Effect systems were originally conceived as an inference-based program analysis to capture program behaviour—as a set of (representations of) effects. Two orthogonal developments have since happened. First, motivated by static analysis, effects were generalised to values in an algebra, to better model control flow (e.g. for may/must analyses and concurrency). Second, motivated by semantic questions, the syntactic notion of set- (or semilattice-) based effect system was linked to the semantic notion of monads and more recently to graded monads which give a more precise semantic account of effects.We give a lightweight tutorial explanation of the concepts involved in these two threads and then unify them via the notion of an effect-directed semantics for a control-flow algebra of effects. For the case of effectful programming with sequencing, alternation and parallelism—illustrated with music—we identify a form of graded joinads as the appropriate structure for unifying effect analysis and semantics.
Xie J, Niu X, Lau AKS, et al., 2015, Accelerated cell imaging and classification on FPGAs for quantitive-phase asymmetric-detection time-stretch optical microscopy, 2015 International Conference on Field-Programmable Technology, Publisher: IEEE, Pages: 1-8
With the fundamental trade-off between speed and sensitivity, existing quantitative phase imaging (QPI) systems for diagnostics and cell classification are often limited to batch processing only small amount of offline data. While quantitative asymmetric-detection time-stretch optical microscopy (Q-ATOM) offers a unique optical platform for ultrafast and high-sensitivity quantitative phase cellular imaging, performing the computationally demanding backend QPI phase retrieval and image classification in real-time remains a major technical challenge. In this paper, we propose an optimized architecture for QPI on FPGA and compare its performance against CPU and GPU implementations in terms of speed and power efficiency. Results show that our implementation on single FPGA card demonstrates a speedup of 9.4 times over an optimized C implementation running on a 6-core CPU, and 3.47 times over the GPU implementation. It is also 24.19 and 4.88 times more power-efficient than the CPU and GPU implementation respectively. Throughput increase linearly when four FPGA cards are used to further improve the performance. We also demonstrate an increased classification accuracy when phase images instead of single-angle ATOM images are used. Overall, one FPGA card is able to process and categorize 2497 cellular images per second, making it suitable for real-time single-cell analysis applications.
López HA, Marques ERB, Martins F, et al., 2015, Protocol-based verification of message-passing parallel programs, OOPSLA 2015, Publisher: ACM, Pages: 280-298
We present ParTypes, a type-based methodology for the verification of Message Passing Interface (MPI) programs written in the C programming language. The aim is to statically verify programs against protocol specifications, enforcing properties such as fidelity and absence of deadlocks. We develop a protocol language based on a dependent type system for message-passing parallel programs, which includes various communication operators, such as point-to-point messages, broadcast, reduce, array scatter and gather. For the verification of a program against a given protocol, the protocol is first translated into a representation read by VCC, a software verifier for C. We successfully verified several MPI programs in a running time that is independent of the number of processes or other input parameters. This contrasts with alternative techniques, notably model checking and runtime verification, that suffer from the state-explosion problem or that otherwise depend on parameters to the program itself. We experimentally evaluated our approach against state-of-the-art tools for MPI to conclude that our approach offers a scalable solution.
López HA, Marques ERB, Martins F, et al., 2015, Protocol-based verification of message-passing parallel programs, SPLASH '15: Conference on Systems, Programming, Languages, and Applications: Software for Humanity, Publisher: ACM
Lopez HA, Marques RBE, Martins F, et al., 2015, Protocol-Based Verification of Message-Passing Parallel Programs, 2015 ACM International Conference on Object Oriented Programming, Systems, Languages & Applications, Publisher: ACM
We present ParTypes, a type-based methodology for the verificationof Message Passing Interface (MPI) programs writtenin the C programming language. The aim is to staticallyverify programs against protocol specifications, enforcingproperties such as fidelity and absence of deadlocks. We developa protocol language based on a dependent type systemfor message-passing parallel programs, which includes variouscommunication operators, such as point-to-point messages,broadcast, reduce, array scatter and gather. For theverification of a program against a given protocol, the protocolis first translated into a representation read by VCC, asoftware verifier for C. We successfully verified several MPIprograms in a running time that is independent of the numberof processes or other input parameters. This contrasts withalternative techniques, notably model checking and runtimeverification, that suffer from the state-explosion problem orthat otherwise depend on parameters to the program itself.We experimentally evaluated our approach against state-ofthe-arttools for MPI to conclude that our approach offers ascalable solution.
Demangeon R, Yoshida N, 2015, On the Expressiveness of Multiparty Session Types, 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science
This paper explores expressiveness of asynchronous multiparty sessions. We model the behaviours ofendpoint implementations in several ways: (i) by the existence of different buffers and queues used tostore messages exchanged asynchronously, (ii) by the ability for an endpoint to lightly reconfigure hisbehaviour at runtime (flexibility), (iii) by the presence of explicit parallelism or interruptions (exceptionalactions) in endpoint behaviour. For a given protocol we define several denotations, based on traces ofevents, corresponding to the different implementations and compare them.
Carbone M, Montesi F, Schürmann C, et al., 2015, Multiparty Session Types as Coherence Proofs, 26th International Conference on Concurrency Theory (CONCUR 2015), Publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl Publishing, Pages: 412-426
We propose a Curry-Howard correspondence between a language for programming multipartysessions and a generalisation of Classical Linear Logic (CLL). In this framework, propositionscorrespond 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 generalisingduality, from CLL, to a new notion of n-ary compatibility, called coherence. Building on coherenceas a principle of compositionality, we generalise the cut rule of CLL to a new rule for composingmany processes communicating in a multiparty session. We prove the soundness of our model byshowing the admissibility of our new rule, which entails deadlock-freedom via our correspondence.
Ng N, Yoshida N, 2015, Pabble: parameterised Scribble, SERVICE ORIENTED COMPUTING AND APPLICATIONS, Vol: 9, Pages: 269-284, ISSN: 1863-2386
- Author Web Link
- Open Access Link
- Cite
- Citations: 15
Moretti NS, Augusto LDS, Clemente TM, et al., 2015, Characterization of <i>Trypanosoma cruzi</i> Sirtuins as Possible Drug Targets for Chagas Disease, ANTIMICROBIAL AGENTS AND CHEMOTHERAPY, Vol: 59, Pages: 4669-4679, ISSN: 0066-4804
- Author Web Link
- Cite
- Citations: 31
Orchard D, Rice A, Oshmyan O, 2015, Evolving Fortran types with inferred units-of-measure, JOURNAL OF COMPUTATIONAL SCIENCE, Vol: 9, Pages: 156-162, ISSN: 1877-7503
- Author Web Link
- Cite
- Citations: 4
Bocchi L, Lange J, Yoshida N, 2015, Meeting Deadlines Together, CONCUR 2015
This paper studies safety, progress, and non-zeno properties of Communicating Timed Automata (CTAs), which are timed automata (TA) extended with unbounded communication channels,and presents a procedure to build timed global specifications from systems of CTAs. We define safety and progress properties for CTAs by extending properties studied in communicating finite-state machines to the timed setting. We then study non-zenoness for CTAs; our aim is to prevent scenarios in which the participants have to execute an infinite number of actions in a finite amount of time. We propose sound and decidable conditions for these properties, and demonstrate thepracticality of our approach with an implementation and experimental evaluations of our theory.
Coppo M, Dezani-Ciancaglini M, Padovani L, et al., 2015, A gentle introduction to multiparty asynchronous session types, 15th International School on Formal Methods for the Design of Computer, Communication and Software Systems: Multicore Programming, Publisher: Springer, Pages: 146-178, ISSN: 0302-9743
This article provides a gentle introduction to multiparty session types, a class of behavioural types specifically targeted at describing protocols in distributed systems based on asynchronous communication. The type system ensures well-typed processes to enjoy non-trivial properties, including communication safety, protocol fidelity, as well as progress. The adoption of multiparty session types can positively affect the whole software lifecycle, from design to deployment, improving software reliability and reducing its development costs.
Orchard D, Rice A, Oshmyan O, 2015, Evolving Fortran types with inferred units-of-measure, Journal of Computational Science, ISSN: 1877-7503
Tiezzi F, Yoshida N, 2015, Reversible Session-Based Pi-Calculus, Journal of Logical and Algebraic Methods in Programming, Vol: 84, Pages: 684-707, ISSN: 2352-2208
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 to take different computation paths along the same session, as well as to revert the whole session and start 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 propose ReSπ a session-based variant of π-calculus using memory devices to keep track of the computation history of sessions in order to reverse it. We show how a session type discipline of π-calculus is extended to ReSπ, and illustrate its practical advantages for static verification of safe composition in communication-centric distributed software performing reversible computations. We also show how a fully reversible characterisation of the calculus extends to committable sessions, where computation can go forward and backward until the session is committed by means of a specific irreversible action.
Yoshida N, Mostrous D, 2015, Session Typing and Asynchronous Subtyping for the Higher-Order π-Calculus, Information and Computation, Vol: 241, Pages: 227-263, ISSN: 1090-2651
This paper proposes a session typing system for the higher-order -calculus (the HOc-calculus) with asynchronous communication subtyping, which allows partial commutativity of actions in higher-order processes. The system enables two complementary kinds of optimisation of communication code, mobile code and asynchronous permutation of session actions, within processes that utilise structured, typed communications. Our first contribution is to establish a session typing system for the higher-order r-calculus using -calculus. Integration of arbitrary higherorder code mobility and sessions leads to technical difficulties in type soundness, because linear usage of session channels and completion of sessions are required in executed code. Our second contribution is to introduce the asynchronous subtyping system which uniformly deals with type-manifested asynchrony and linear functional types. The most technical challenge for the asynchronous subtyping is to prove the transitivity of the subtyping relation. For the runtime system we propose a new compact formulation that takes into account stored higher-order values with open sessions, as well as asynchronous commutativity. The paper also demonstrates the expressiveness of our typing system with an e-commerce example, where optimised processes can interact respecting the expected sessions.
Lange J, Tuosto E, Yoshida N, 2015, From communicating machines to graphical choreographies, 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Publisher: Association for Computing Machinery, Pages: 221-232, ISSN: 1523-2867
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.
Lange J, Tuosto E, Yoshida N, 2015, From Communicating Machines to Graphical Choreographies, POPL '15: The 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Publisher: ACM
Kouzapas D, Pérez JA, Yoshida N, 2015, Core higher-order session processes: tractable equivalences and relative expressiveness, Departmental Technical Report: 15/1, Publisher: Department of Computing, Imperial College London, 15/1
This work proposes tractable bisimulations for the higher-order -calculus with session primitives (HO ) and o ers a complete study of the expressivityof its most significant subcalculi. First we develop three typed bisimulations,which are shown to coincide with contextual equivalence. These characterisationsdemonstrate that observing as inputs only a specific finite set ofhigher-order values (which inhabit session types) su ces to reason about HO processes. Next, we identify HO, a minimal, second-order subcalculus of HO in which higher-order applications/abstractions, name-passing, and recursion areabsent. We show that HO can encode HO extended with higher-order applicationsand abstractions and that a first-order session -calculus can encode HO .Both encodings are fully abstract. We also prove that the session -calculus withpassing of shared names cannot be encoded into HO without shared names. Weshow that HO , HO, and are equally expressive; the expressivity of HO enablese ective reasoning about typed equivalences for higher-order processes.
Cogumbreiro T, Hu R, Martins F, et al., 2015, Dynamic Deadlock Verification for General Barrier Synchronisation, 20th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming (PPoPP), Publisher: ASSOC COMPUTING MACHINERY, Pages: 150-160
Scalas A, Yoshida N, 2015, Lightweight session programming in scala, Departmental Technical Report: 15/7, Publisher: Department of Computing, Imperial College London, 15/7
Designing, developing and maintaining concurrent applications is an error-prone and time-consumingtask; most difficulties arise because compilers are usually unable to check whether theinputs/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 thenative features of the Scala type system and standard library, to introduce (1) a representationof session types as Scala types, and (2) a library, called lchannels, with a convenient API forsession-based programming, supporting local and distributed communication. We generalise theidea of Continuation-Passing Style Protocols (CPSPs), studying their formal relationship withsession types. We illustrate how session programming can be carried over in Scala: how toformalise a communication protocol, and represent it using Scala classes and lchannels, lettingthe compiler help spotting protocol violations. We attest the practicality of our approach with acomplex use case, and evaluate the performance of lchannels with a series of benchmarks.
Hu R, Yoshida N, 2015, Hybrid session veri cation through endpoint API generation, Departmental Technical Report: 15/6, Publisher: Department of Computing, Imperial College London, 15/6
This paper proposes a new hybrid session veri cation method-ology for applying session types directly to mainstream languages, basedon generating protocol-speci c endpoint APIs from multiparty sessiontypes. The API generation promotes static type checking of the be-havioural aspect of the source protocol by mapping the state space ofan endpoint in the protocol to a family of channel types in the tar-get language. This is supplemented by very light run-time checks in thegenerated API that enforce a linear usage discipline on instances of thechannel types. The resulting hybrid veri cation guarantees the absenceof protocol violation errors during the execution of the session. We haveimplemented our methodology for Java as an extension to the Scrib-ble framework, and used it to implement compliant clients and serversfor real-world protocols such as HTTP and SMTP. The API genera-tion methodology additionally provides a platform for applying furtherfeatures from session type theory: our implementation supports choicesubtyping through branch interface generation, and safe permutation ofI/O actions and a ne inputs through input future generation.
Kouzapas D, Yoshida N, 2014, Globally governed session semantics, Logical Methods in Computer Science, Vol: 10, Pages: 1-45, ISSN: 1860-5974
This paper proposes a bisimulation theory based on multiparty session types where a choreography specification governs the behavior 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 optimizations 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.
Fossati L, Hu R, Yoshida N, 2014, Multiparty Session Nets, 9th International Symposium on Trustworthy Global Computing, Publisher: Springer, Pages: 112-127, ISSN: 0302-9743
Yoshida N, Ng N, Coutinho JGF, 2014, Protocols by Default: Safe MPI Code Generation based on Session Types, 24th International Conference on Compiler Construction (CC 2015), Publisher: Springer, Pages: 212-232
This paper presents a code generation framework for type-safe and deadlock-free Message Passing Interface (MPI) programs. The code generation process starts with the definition of the global topology using a protocol specification language based on parameterised multiparty session types (MPST). An MPI parallel program backbone is automatically generated from the global specification. The backbone code can then be merged with the sequential code describing the application behaviour, resulting in a complete MPI program. This merging process is fully automated through the use of an aspect-oriented compilation approach. In this way, programmers only need to supply the intended communication protocol and provide sequential code to automatically obtain parallelised programs that are guaranteed free from communication mismatch, type errors or deadlocks. The code generation framework also integrates an optimisation method that overlaps communication and computation, and can derive not only representative parallel programs with common parallel patterns (such as ring and stencil), but also distributed applications from any MPST protocols. We show that our tool generates efficient and scalable MPI applications, and improves productivity of programmers. For instance, our benchmarks involving representative parallel and application-specific patterns speed up sequential execution by up to 31 times and reduce programming effort by an average of 39%.
Maeda FY, Cortez C, Izidoro MA, et al., 2014, Fibronectin-Degrading Activity of <i>Trypanosoma cruzi</i> Cysteine Proteinase Plays a Role in Host Cell Invasion, INFECTION AND IMMUNITY, Vol: 82, Pages: 5166-5174, ISSN: 0019-9567
- Author Web Link
- Cite
- Citations: 14
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.