79 research outputs found
Concurrency with Weak Memory Models (Dagstuhl Seminar 16471)
No full textThis report documents the program and the outcomes of Dagstuhl Seminar 16471 "Concurrency with Weak Memory Models: Semantics, Languages, Compilation, Verification, Static Analysis, and Synthesis". The aim of the seminar was to bring together people from various horizons, including theoreticians and verification practitioners as well as hardware vendors, in order to set up a long-term research program to design formal methods and develop tools ensuring the correctness of concurrent programs on modern multi-processor architectures
GPU Concurrency: Weak Behaviours and Programming Assumptions
No full textConcurrency is pervasive and perplexing, particularly on graphics processing units (GPUs). Current specifications of languages and hardware are inconclusive; thus programmers often rely on folklore assumptions when writing software.
To remedy this state of affairs, we conducted a large empirical study of the concurrent behaviour of deployed GPUs. Armed with litmus tests (i.e. short concurrent programs), we questioned the assumptions in programming guides and vendor documentation about the guarantees provided by hardware. We developed a tool to generate thousands of litmus tests and run them under stressful workloads. We observed a litany of previously elusive weak behaviours, and exposed folklore beliefs about GPU programming---often supported by official tutorials---as false.
As a way forward, we propose a model of Nvidia GPU hardware, which correctly models every behaviour witnessed in our experiments. The model is a variant of SPARC Relaxed Memory Order (RMO), structured following the GPU concurrency hierarchy
Software Verification for Weak Memory via Program Transformation
No full textThis version previously deposited at arXiv:1207.7264v1 [cs.LO
Partial Orders for Efficient BMC of Concurrent Software
No full textThis version previously deposited at arXiv:1301.1629v1 [cs.LO]The vast number of interleavings that a concurrent program can have is typically identified as the root cause of the difficulty of automatic analysis of concurrent software. Weak memory is generally believed to make this problem even harder. We address both issues by modelling programs' executions with partial orders rather than the interleaving semantics (SC). We implemented a software analysis tool based on these ideas. It scales to programs of sufficient size to achieve first-time formal verification of non-trivial concurrent systems code over a wide range of models, including SC, Intel x86 and IBM Power
Broadcast and Aggregation in BBC
No full textIn this paper we introduce a process calculus BBC that has both forms of communication. For both many-to-one and one-to-many communication, it is often a natural assumption that communication is bounded; this reflects two distinct aspects of the limitations of a medium. In the case of broadcast, the bound limits the number of possible recipients of a message. In the case of collection, the bound limits the number of messages that can be received. For this reason, BBC uses a notion of bounded broadcast and collection. Moreover, the syntax of the calculus introduces an explicit notion of connectivity that makes it possible to represent a communication topology directly. By using a proof technique introduced by Palamidessi we show that even a version of BBC that only uses collection is more expressive than the pi-calculus
Static analyses over weak memory
No full textWriting concurrent programs with shared memory is often not trivial. Correctly synchronising the threads and handling the non-determinism of executions require a good understanding of the interleaving semantics. Yet, interleavings are not sufficient to model correctly the executions of modern, multicore processors. These executions follow rules that are weaker than those observed by the interleavings, often leading to reorderings in the sequence of updates and readings from memory; the executions are subject to a weaker memory consistency. Reorderings can produce executions that would not be observable with interleavings, and these possible executions also depend on the architecture that the processors implement. It is therefore necessary to locate and understand these reorderings in the context of a program running, or to prevent them in an automated way. In this dissertation, we aim to automate the reasoning behind weak memory consistency and perform transformations over the code so that developers need not to consider all the specifics of the processors when writing concurrent programs. We claim that we can do automatic static analysis for axiomatically-defined weak memory models. The method that we designed also allows re-use of automated verification tools like model checkers or abstract interpreters that were not designed for weak memory consistency, by modification of the input programs. We define an abstraction in detail that allows us to reason statically about weak memory models over programs. We locate the parts of the code where the semantics could be affected by the weak memory consistency. We then provide a method to explicitly reveal the resulting reorderings so that usual verification techniques can handle the program semantics under a weaker memory consistency. We finally provide a technique that synthesises synchronisations so that the program would behave as if only interleavings were allowed. We finally test these approaches on artificial and real software. We justify our choice of an axiomatic model with the scalability of the approach and the runtime performance of the programs modified by our method
- …
