1,721,328 research outputs found
Reversible session-based pi-calculus
Full text linkIn 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 ReSpi a session-based variant of pi-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 pi-calculus is extended to ReSpi, 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
Checkpoint-based rollback recovery in session programming
Full text linkTo react to unforeseen circumstances or amend abnormal situations in
communication-centric systems, programmers are in charge of "undoing" the
interactions which led to an undesired state. To assist this task,
session-based languages can be endowed with reversibility mechanisms. In this
paper we propose a language enriched with programming facilities to commit
session interactions, to roll back the computation to a previous commit point,
and to abort the session. Rollbacks in our language always bring the system to
previous visited states and a rollback cannot bring the system back to a point
prior to the last commit. Programmers are relieved from the burden of ensuring
that a rollback never restores a checkpoint imposed by a session participant
different from the rollback requester. Such undesired situations are prevented
at design-time (statically) by relying on a decidable compliance check at the
type level, implemented in MAUDE. We show that the language satisfies
error-freedom and progress of a session
A gentle introduction to multiparty asynchronous session types
Full text linkThis 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
Unravelling T. cruzi Biology
No full textThis eBook is a collection of articles from a Frontiers Research Topic. Frontiers Research Topics are very popular trademarks of the Frontiers Journals Series: they are collections of at least ten articles, all centered on a particular subject. With their unique mix of varied contributions from Original Research to Review Articles, Frontiers Research Topics unify the most influential researchers, the latest key findings and historical advances in a hot research area! Find out more on how to host your own Frontiers Research Topic or contribute to one as an author by contacting the Frontiers Editorial Office: frontiersin.org/about/contac
Unravelling T. cruzi Biology
No full textThis eBook is a collection of articles from a Frontiers Research Topic. Frontiers Research Topics are very popular trademarks of the Frontiers Journals Series: they are collections of at least ten articles, all centered on a particular subject. With their unique mix of varied contributions from Original Research to Review Articles, Frontiers Research Topics unify the most influential researchers, the latest key findings and historical advances in a hot research area! Find out more on how to host your own Frontiers Research Topic or contribute to one as an author by contacting the Frontiers Editorial Office: frontiersin.org/about/contac
Proceedings of the First Workshop on Programming Language Approaches to Concurrency and Communication-cEntric Software
No full textThis documents contains the proceedings of PLACES'08, the 1st Workshop on Programming Language Approaches to Concurrency and Communication- cEntric Software, held in Oslo, Norway, on June 7, 2008, co-located with the DisCoTec federated conferences. PLACES aims to offer a forum where researchers from different Þelds ex- change new ideas on one of the central challenges in programming in near future, the development of programming methodologies and infrastructures where con- currency and distribution are a norm rather than a marginal concern. The Program Committee, after a careful and thorough reviewing process, se- lected for inclusion in the programme 10 papers out of 14 submissions. Each submission was evaluated by at least two referees, and the accepted papers were selected during one week electronic discussions. The volume opens with the abstracts for the invited contributions by Jan Vitek (Purdue University) and and Alan Mycroft (University of Cambridge), and con- tinues with the ten technical papers. Places'08 was made possible by the contribution and dedication of many peo- ple. First of all, we would like to thank all the authors who submitted papers for consideration. Secondly we would like to thank our invited and tutorial speakers. We would also like to thank the members of the Program Committee for their care- ful reviews, and the balanced discussions during the selection process. Dimitris Mostrous helped to set up a web page for the PC discussion. Finally, we acknowl- edge the Discotec general chairs, Frank Eliassen and Einar Broch Johnsen, and the Workshop chair Amy L. Murph
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
A Study of Bisimulation Theory for Session Types
Full text linkBisimulation theory is a co-inductive tool used as a tractable method for studying equivalence
relations in process calculi. This dissertation studies bisimulation theory for session types. We
define the Asynchronous Session π-calculus (ASP for short), which is a session type calculus
with queue configurations acting as a communication medium at each session endpoint The
semantics for ASP offer fine-grained communication that enjoys the non-blocking property
of asynchrony and the order-preserving property of session types. The ASP typing system is
shown to be sound to guarantee type safety in the presence of subtyping. A typed labelled
transition system gives rise to a bisimilarity which is sound and complete with respect to typed
reduction-closed congruence. The bisimilarity theory of ASP highlights the determinacy and
confluence properties of session types.
Event-driven programming is one of the major paradigms that utilise the asynchronous nature
of distributed systems, where events are recognised as the presence of messages and their
typed information in the communication medium. To justify the design choices made, we
develop a superset of ASP, called the Eventful Session π-calculus (ESP for short), equipped
with the minimal session primitives for an expressive event-driven computational model. The
eventful session type system introduces the session set type, which is a collection of session
types used to type a set of possible events. The ESP typing system maintains its consistency
with respect to the ASP session typing system up-to a subtyping relation for session set types.
The straightforward extension from ASP to ESP offers behavioural transparency, making the
bisimilarity theory for the ASP a special case for the ESP theory – the bisimilarity relation
coincides with typed reduction-closed congruence and determinacy and confluence properties
are shown to hold for session transitions.
Many studies regarding event-driven computation have identified the selector or its equivalent,
the polling operator, as the key construct for describing an event-driven framework. The
selector is defined as a higher level construct in ESP and it is used to implement the core event
handling routine called the event loop. Following the empirical study by Lauer and Needham,
we define a session-based transformation from a multi-threaded server to an event loop server.
Confluence theory proves that the transformation is type- and semantics-preserving.
In the last part of the dissertation we extend the behavioural theory to multiparty session
types, both in the synchronous and the asynchronous cases. For each case, we examine two
different typed labelled transition systems. In the first case we examine a standard labelled
transition system with respect to the local session typing of processes. In the second case
a choreography specification governs the behaviour of a multiparty session process and its
observer. Each labelled transition system defines a bisimilarity relation, which coincides with
the corresponding reduction-closed congruence.Open Acces
- …
