1,721,389 research outputs found
Timed Runtime Monitoring for Multiparty Conversations
Full text linkWe 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, 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 constraining the times in which interactions should 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. The performance of our implementation and its practicability are analysed via benchmarking
Refinements for Multiparty Message-Passing Protocols: Specification-Agnostic Theory and Implementation (Artifact)
Full text linkMultiparty message-passing protocols are notoriously difficult to design, due to interaction mismatches that lead to errors such as deadlocks. Existing protocol specification formats have been developed to prevent such errors (e.g. multiparty session types (MPST)). In order to further constrain protocols, specifications can be extended with refinements, i.e. logical predicates to control the behaviour of the protocol based on previous values exchanged. Unfortunately, existing refinement theories and implementations are tightly coupled with specification formats.
This artifact accompanies [Martin Vassor and Nobuko Yoshida, 2024]. It presents an implementation of the framework presented in this paper
Stay Safe Under Panic: Affine Rust Programming with Multiparty Session Types (Artifact)
Full text linkThis artifact contains a version of MultiCrusty, a Rust library designed for writing and checking communication protocols following the Affine Multiparty Session Types theory introduced in our ECOOP'22 paper. MultiCrusty can work, and should be used, with Scribble [Yoshida et al., 2014] and kMC [{Julien} {Lange} and {Nobuko} {Yoshida}, 2019]: with the former tool, users can write correct global protocols and project them onto local Rust types defined within MultiCrusty, this approach is qualified as top-down; while the latter tool allows to check local Rust types written by users, this approach is qualified as bottom-up. Our artifact contains those three tools, their respective source files, as well as the different examples and benchmarks introduced in our paper, all together within a Docker image
PLACES'10: The 3rd Workshop on Programmng Language Approaches to concurrency and Communication-Centric Software
No full textPaphos, Cyprus. March 201
Type and Effect Systems for Dynamically Changing Code - DRAFT CORRECTIONS, DO NOT DISTRIBUTE
No full textWe extend type and effect analyses to permit dynamically changing effects and dynamically changing code in multi-threaded systems with shared resources. We guarantee that after a well typed modification a set of threads will have the specified desired effects and will continue to safely use the resources. We prove the key properties of subject reduction and fidelity (safety) for our general system. We provide an application of our system: dynamic software updating for a multi-threaded asynchronous message passing system. We show how key safety properties from session typing follow from the properties of our general system
Channel Dependent Types for Higher-Order Mobile Processes (Extended Abstract)
No full textNobuko Yoshida Imperial College London ABSTRACT We introduce a new expressive theory of types for the higher-order p-calculus and demonstrate its applicability via non-trivial security analyses of a simple class-based language with distributed code mobility. The new theory significantly improves our previous one presented in [52] by the use of channel dependent/existential types. New dependent types control dynamic change of process accessibility via channel passing, while existential types guarantee safe scope-extrusion in higher-order process passing. This solves an open issue in [52], leading to significant enlargement of original typability. Two basic security concerns for mobile computation, secrecy for data confidentiality and access controls for authorised resources are analysed in a uniform type-based static framework, culminating in the noninterference theorem and authority-error freedom in the presence of higher-order code mobility. The generality and expressiveness of the new type discipline are tested with a sound embedding of multi-threaded class-based language with dynamic code/class distribution, enforcing secrecy and accessibility
Global Progress for Dynamically Interleaved Multiparty Sessions
No full textA 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
CONCUR test-of-time award for the period 1994–97 interview with uwe nestmann and Benjamin C. Pierce
Full text linkLast year, the CONCUR conference series inaugurated its Test-of-Time Award,
the purpose of which is to recognise important achievements in Concurrency
Theory that were published at the conference and have stood the test of time.
This year, Decoding Choice Encodings by Uwe Nestmann and Benjamin C.
Pierce was one of four papers chosen to receive the CONCUR Test-of-Time
Award for the periods 1994–1997 and 1996–1999 by a jury consisting of Rob
van Glabbeek (chair), Luca de Alfaro, Nathalie Bertrand, Catuscia Palamidessi,
and Nobuko Yoshida. This article is devoted to the engaging and interesting
interview conducted with Uwe Nestmann and Benjamin C. Pierce via video
conference
Going Beyond Counting First Authors in Author Co-citation Analysis
Full text linkThe present study examines one of the fundamental aspects of author co-citation analysis (ACA) - the way co-citation
counts are defined. Co-citation counting provides the data on which all subsequent statistical analyses and mappings
are based, and we compare ACA results based on two different types of co-citation counting - the traditional type that
only counts the first one among a cited work's authors on the one hand and a non-traditional type that takes into
account the first 5 authors of a cited work on the other hand. Results indicate that the picture produced through this non-traditional author co-citation counting contains more coherent author groups and is therefore considerably clearer. However, this picture represents fewer specialties in the research field being studied than that produced through the traditional first-author co-citation counting when the same number of top-ranked authors is selected and analyzed. Reasons for these effects are discussed
- …
