Transactional events

2008 ◽  
Vol 18 (5-6) ◽  
pp. 649-706 ◽  
Author(s):  
KEVIN DONNELLY ◽  
MATTHEW FLUET
Keyword(s):  
Message Passing ◽  
Formal Semantics ◽  
Concurrent Programming ◽  
Expressive Power ◽  
Detailed Account ◽  
Concurrent Programs ◽  
Compositional Reasoning ◽  
Compositional Structure ◽  
High Level

AbstractConcurrent programs require high-level abstractions in order to manage complexity and enable compositional reasoning. In this paper, we introduce a novel concurrency abstraction, dubbed transactional events, which combines first-class synchronous message passing events with all-or-nothing transactions. This combination enables simple solutions to interesting problems in concurrent programming. For example, guarded synchronous receive can be implemented as an abstract transactional event, whereas in other languages it requires a non-abstract, non-modular protocol. As another example, three-way rendezvous can be implemented as an abstract transactional event, which is impossible using first-class events alone. Both solutions are easy to code and easy to reason about.The expressive power of transactional events arises from a sequencing combinator whose semantics enforces an all-or-nothing transactional property – either both of the constituent events synchronize in sequence or neither of them synchronizes. This sequencing combinator, along with a non-deterministic choice combinator, gives transactional events the compositional structure of a monad-with-plus. We provide a formal semantics for transactional events and give a detailed account of an implementation.

Causal-Consistent Replay Reversible Semantics for Message Passing Concurrent Programs

2021 ◽  
Vol 178 (3) ◽  
pp. 229-266
Author(s):  
Ivan Lanese ◽  
Adrián Palacios ◽  
Germán Vidal
Keyword(s):  
Programming Language ◽  
Message Passing ◽  
Concurrent Programming ◽  
Concurrent Systems ◽  
Concurrent Programs ◽  
Unified Framework ◽  
Innovative Technique ◽  
Dual Notion

Causal-consistent reversible debugging is an innovative technique for debugging concurrent systems. It allows one to go back in the execution focusing on the actions that most likely caused a visible misbehavior. When such an action is selected, the debugger undoes it, including all and only its consequences. This operation is called a causal-consistent rollback. In this way, the user can avoid being distracted by the actions of other, unrelated processes. In this work, we introduce its dual notion: causal-consistent replay. We allow the user to record an execution of a running program and, in contrast to traditional replay debuggers, to reproduce a visible misbehavior inside the debugger including all and only its causes. Furthermore, we present a unified framework that combines both causal-consistent replay and causal-consistent rollback. Although most of the ideas that we present are rather general, we focus on a popular functional and concurrent programming language based on message passing: Erlang.

scholarly journals Evolution of the ALICE Software Framework for Run 3

2019 ◽  
Vol 214 ◽  
pp. 05010 ◽  
Author(s):  
Giulio Eulisse ◽  
Piotr Konopka ◽  
Mikolaj Krzewicki ◽  
Matthias Richter ◽  
David Rohr ◽  
...  
Keyword(s):  
Data Processing ◽  
Data Model ◽  
Message Passing ◽  
Software Framework ◽  
Distributed Software ◽  
Central Collisions ◽  
Modular Software ◽  
Level Trigger ◽  
Data Throughput ◽  
High Level

ALICE is one of the four major LHC experiments at CERN. When the accelerator enters the Run 3 data-taking period, starting in 2021, ALICE expects almost 100 times more Pb-Pb central collisions than now, resulting in a large increase of data throughput. In order to cope with this new challenge, the collaboration had to extensively rethink the whole data processing chain, with a tighter integration between Online and Offline computing worlds. Such a system, code-named ALICE O2, is being developed in collaboration with the FAIR experiments at GSI. It is based on the ALFA framework which provides a generalized implementation of the ALICE High Level Trigger approach, designed around distributed software entities coordinating and communicating via message passing. We will highlight our efforts to integrate ALFA within the ALICE O2 environment. We analyze the challenges arising from the different running environments for production and development, and conclude on requirements for a flexible and modular software framework. In particular we will present the ALICE O2 Data Processing Layer which deals with ALICE specific requirements in terms of Data Model. The main goal is to reduce the complexity of development of algorithms and managing a distributed system, and by that leading to a significant simplification for the large majority of the ALICE users.

scholarly journals Coloring Graph Neural Networks for Node Disambiguation

2020 ◽  
Author(s):  
George Dasoulas ◽  
Ludovic Dos Santos ◽  
Kevin Scaman ◽  
Aladin Virmaux
Keyword(s):  
Neural Networks ◽  
Message Passing ◽  
State Of The Art ◽  
Structural Characteristics ◽  
Expressive Power ◽  
Continuous Functions ◽  
Graph Classification ◽  
Node Attributes ◽  
Graph Neural Networks ◽  
Coloring Graph

In this paper, we show that a simple coloring scheme can improve, both theoretically and empirically, the expressive power of Message Passing Neural Networks (MPNNs). More specifically, we introduce a graph neural network called Colored Local Iterative Procedure (CLIP) that uses colors to disambiguate identical node attributes, and show that this representation is a universal approximator of continuous functions on graphs with node attributes. Our method relies on separability, a key topological characteristic that allows to extend well-chosen neural networks into universal representations. Finally, we show experimentally that CLIP is capable of capturing structural characteristics that traditional MPNNs fail to distinguish, while being state-of-the-art on benchmark graph classification datasets.

scholarly journals TaDA Live: Compositional Reasoning for Termination of Fine-grained Concurrent Programs

2021 ◽  
Vol 43 (4) ◽  
pp. 1-134
Author(s):  
Emanuele D’Osualdo ◽  
Julian Sutherland ◽  
Azadeh Farzan ◽  
Philippa Gardner
Keyword(s):  
Case Studies ◽  
Separation Logic ◽  
Proof System ◽  
Concurrent Programs ◽  
Semantic Model ◽  
Compositional Reasoning ◽  
Fine Grained ◽  
Fundamental Innovation ◽  
Concurrent Separation Logic

We present TaDA Live, a concurrent separation logic for reasoning compositionally about the termination of blocking fine-grained concurrent programs. The crucial challenge is how to deal with abstract atomic blocking : that is, abstract atomic operations that have blocking behaviour arising from busy-waiting patterns as found in, for example, fine-grained spin locks. Our fundamental innovation is with the design of abstract specifications that capture this blocking behaviour as liveness assumptions on the environment. We design a logic that can reason about the termination of clients that use such operations without breaking their abstraction boundaries, and the correctness of the implementations of the operations with respect to their abstract specifications. We introduce a novel semantic model using layered subjective obligations to express liveness invariants and a proof system that is sound with respect to the model. The subtlety of our specifications and reasoning is illustrated using several case studies.

M-nets: An algebra of high-level Petri nets, with an application to the semantics of concurrent programming languages

1998 ◽  
Vol 35 (10) ◽  
pp. 813-857 ◽  
Author(s):  
Eike Best ◽  
Wojciech Frączak ◽  
Richard P. Hopkins ◽  
Hanna Klaudel ◽  
Elisabeth Pelz
Keyword(s):  
Petri Nets ◽  
Programming Languages ◽  
Concurrent Programming ◽  
Concurrent Programming Languages ◽  
High Level

scholarly journals Compact Modeling Framework v3.0 for high-resolution global ocean–ice–atmosphere models

2018 ◽  
Vol 11 (10) ◽  
pp. 3983-3997 ◽  
Author(s):  
Vladimir V. Kalmykov ◽  
Rashit A. Ibrayev ◽  
Maxim N. Kaurkin ◽  
Konstantin V. Ushakov
Keyword(s):  
Message Passing ◽  
Message Passing Interface ◽  
Global Ocean ◽  
Optimal Interpolation ◽  
Compact Modeling ◽  
Software Environment ◽  
Modeling Framework ◽  
Partitioned Global Address Space ◽  
Version 2.0 ◽  
High Level

Abstract. We present a new version of the Compact Modeling Framework (CMF3.0) developed for the software environment of stand-alone and coupled global geophysical fluid models. The CMF3.0 is designed for use on high- and ultrahigh-resolution models on massively parallel supercomputers.The key features of the previous CMF, version 2.0, are mentioned to reflect progress in our research. In CMF3.0, the message passing interface (MPI) approach with a high-level abstract driver, optimized coupler interpolation and I/O algorithms is replaced with the Partitioned Global Address Space (PGAS) paradigm communications scheme, while the central hub architecture evolves into a set of simultaneously working services. Performance tests for both versions are carried out. As an addition, some information about the parallel realization of the EnOI (Ensemble Optimal Interpolation) data assimilation method and the nesting technology, as program services of the CMF3.0, is presented.

Sign in / Sign up

Export Citation Format

Share Document