scholarly journals Making weak memory models fair

2021 ◽  
Vol 5 (OOPSLA) ◽  
pp. 1-27
Author(s):  
Ori Lahav ◽  
Egor Namakonov ◽  
Jonas Oberhauser ◽  
Anton Podkopaev ◽  
Viktor Vafeiadis
Keyword(s):  
Declarative Memory ◽  
Mutual Exclusion ◽  
Memory Models ◽  
Memory Model ◽  
Concurrent Programs ◽  
Sequential Consistency ◽  
Formal Proofs ◽  
Liveness Properties ◽  
Uniform Definition ◽  
Fairness Condition

Liveness properties, such as termination, of even the simplest shared-memory concurrent programs under sequential consistency typically require some fairness assumptions about the scheduler. Under weak memory models, we observe that the standard notions of thread fairness are insufficient, and an additional fairness property, which we call memory fairness, is needed. In this paper, we propose a uniform definition for memory fairness that can be integrated into any declarative memory model enforcing acyclicity of the union of the program order and the reads-from relation. For the well-known models, SC, x86-TSO, RA, and StrongCOH, that have equivalent operational and declarative presentations, we show that our declarative memory fairness condition is equivalent to an intuitive model-specific operational notion of memory fairness, which requires the memory system to fairly execute its internal propagation steps. Our fairness condition preserves the correctness of local transformations and the compilation scheme from RC11 to x86-TSO, and also enables the first formal proofs of termination of mutual exclusion lock implementations under declarative weak memory models.

scholarly journals Dartagnan: Bounded Model Checking for Weak Memory Models (Competition Contribution)

2020 ◽  
pp. 378-382
Author(s):  
Hernán Ponce-de-León ◽  
Florian Furbach ◽  
Keijo Heljanko ◽  
Roland Meyer
Keyword(s):  
Model Checking ◽  
Bounded Model Checking ◽  
Memory Models ◽  
Memory Model ◽  
Complete Analysis ◽  
Concurrent Programs ◽  
Sequential Consistency ◽  
Model Checker ◽  
Safety Properties ◽  
C Programs

Abstract Dartagnanis a bounded model checker for concurrent programs under weak memory models. What makes it different from other tools is that the memory model is not hard-coded inside Dartagnanbut taken as part of the input. For SV-COMP’20, we take as input sequential consistency (i.e. the standard interleaving memory model) extended by support for atomic blocks. Our point is to demonstrate that a universal tool can be competitive and perform well in SV-COMP. Being a bounded model checker, Dartagnan’s focus is on disproving safety properties by finding counterexample executions. For programs with bounded loops, Dartagnanperforms an iterative unwinding that results in a complete analysis. The SV-COMP’20 version of Dartagnanworks on Boogiecode. The C programs of the competition are translated internally to Boogieusing SMACK.

scholarly journals The reads-from equivalence for the TSO and PSO memory models

2021 ◽  
Vol 5 (OOPSLA) ◽  
pp. 1-30
Author(s):  
Truc Lam Bui ◽  
Krishnendu Chatterjee ◽  
Tushar Gautam ◽  
Andreas Pavlogiannis ◽  
Viktor Toman
Keyword(s):  
Model Checking ◽  
Polynomial Time ◽  
Memory Models ◽  
Experimental Results ◽  
Concurrent Programs ◽  
Algorithmic Problem ◽  
Sequential Consistency ◽  
Process Communication ◽  
Consistency Verification ◽  
Inter Process Communication

The verification of concurrent programs remains an open challenge due to the non-determinism in inter-process communication. One recurring algorithmic problem in this challenge is the consistency verification of concurrent executions. In particular, consistency verification under a reads-from map allows to compute the reads-from (RF) equivalence between concurrent traces, with direct applications to areas such as Stateless Model Checking (SMC). Importantly, the RF equivalence was recently shown to be coarser than the standard Mazurkiewicz equivalence, leading to impressive scalability improvements for SMC under SC (sequential consistency). However, for the relaxed memory models of TSO and PSO (total/partial store order), the algorithmic problem of deciding the RF equivalence, as well as its impact on SMC, has been elusive. In this work we solve the algorithmic problem of consistency verification for the TSO and PSO memory models given a reads-from map, denoted VTSO-rf and VPSO-rf, respectively. For an execution of n events over k threads and d variables, we establish novel bounds that scale as n k +1 for TSO and as n k +1 · min( n k 2 , 2 k · d ) for PSO. Moreover, based on our solution to these problems, we develop an SMC algorithm under TSO and PSO that uses the RF equivalence. The algorithm is exploration-optimal , in the sense that it is guaranteed to explore each class of the RF partitioning exactly once, and spends polynomial time per class when k is bounded. Finally, we implement all our algorithms in the SMC tool Nidhugg, and perform a large number of experiments over benchmarks from existing literature. Our experimental results show that our algorithms for VTSO-rf and VPSO-rf provide significant scalability improvements over standard alternatives. Moreover, when used for SMC, the RF partitioning is often much coarser than the standard Shasha-Snir partitioning for TSO/PSO, which yields a significant speedup in the model checking task.

scholarly journals Improving the integrative memory model by integrating the temporal dynamics of memory

2019 ◽  
Vol 42 ◽  
Author(s):  
Jonathan Curot ◽  
Emmanuel J. Barbeau
Keyword(s):  
Brain Injury ◽  
Large Scale ◽  
Temporal Dynamics ◽  
Declarative Memory ◽  
Memory Model

Abstract Despite highlighting the role of the attribution system and proposing a coherent large-scale architecture of declarative memory, the integrative memory model would be more “integrative” if the temporal dynamics of the interactions between its components was clarified. This is necessary to make predictions in patients with brain injury and hypothesize dissociations.

scholarly journals Gillian, Part II: Real-World Verification for JavaScript and C

2021 ◽  
pp. 827-850
Author(s):  
Petar Maksimović ◽  
Sacha-Élie Ayoun ◽  
José Fragoso Santos ◽  
Philippa Gardner
Keyword(s):  
Real World ◽  
Symbolic Analysis ◽  
Memory Models ◽  
Separation Logic ◽  
Target Language ◽  
Memory Model ◽  
Analysis Tools

AbstractWe introduce verification based on separation logic to Gillian, a multi-language platform for the development of symbolic analysis tools which is parametric on the memory model of the target language. Our work develops a methodology for constructing compositional memory models for Gillian, leading to a unified presentation of the JavaScript and C memory models. We verify the JavaScript and C implementations of the AWS Encryption SDK message header deserialisation module, specifically designing common abstractions used for both verification tasks, and find two bugs in the JavaScript and three bugs in the C implementation.

scholarly journals Can We Efficiently Check Concurrent Programs Under Relaxed Memory Models in Maude?

2014 ◽  
pp. 21-41 ◽  
Author(s):  
Yehia Abd Alrahman ◽  
Marina Andric ◽  
Alessandro Beggiato ◽  
Alberto Lluch Lafuente
Keyword(s):  
Memory Models ◽  
Concurrent Programs ◽  
Relaxed Memory

scholarly journals The angular gyrus model of consciousness

2013 ◽  
Author(s):  
Graeme E Smith
Keyword(s):  
White Matter ◽  
Temporal Lobe ◽  
Medial Temporal Lobe ◽  
Declarative Memory ◽  
Angular Gyrus ◽  
Memory Model ◽  
White Matter Tracts ◽  
Parietal Lobes ◽  
Intersection Area ◽  
The Brain

The Angular Gyrus sits at the point where the Temporal and Parietal Lobes join. It is a point where integrative processes link together the Where and What pathways through the brain and link them to time. It is also the most likely location for at least two centers of consciousness. In this article the location is discussed and it's potential for a model of consciousness that replaces the Declarative Memory Model of Consciousness previously put forward. It's main benefit over the Declarative Memory Model of Consciousness is that it allows for the preservation of consciousness despite the loss of declarative memory in the cases of Medial Temporal Lobe injury/disease. However Connectome studies might support this model in that the TemporoParietal Fiber Intersection Area provides 7 different white matter tracts that intersect in this area.

scholarly journals A Declarative Memory Model of Evaluative Conditioning

2018 ◽  
Vol 13 (3) ◽  
Author(s):  
Anne Gast
Keyword(s):  
Conditioned Stimulus ◽  
Empirical Evidence ◽  
Attitude Change ◽  
Memory Trace ◽  
Declarative Memory ◽  
Evaluative Conditioning ◽  
Memory Model ◽  
Memory Research ◽  
The Us ◽  
Valence Change

I propose a Declarative Memory Model (DMM) of evaluative conditioning (EC). EC effects are changes in the valence of a conditioned stimulus (CS) due to previous pairings with a positive or negative unconditioned stimulus (US; e.g., De Houwer, 2007, https://doi.org/10.1017/S1138741600006491). According to the DMM, EC effects are found if (1) a memory trace is formed in the learning phase that links the CS to evaluative information from the US, if (2) this trace survives the retention interval, if (3) the trace or part of it is consciously retrieved when the CS is being evaluated, and if (4) the retrieved trace is used in the CS evaluation. For each of these stages, I make separate predictions about EC effects, many of which are based on empirical research on declarative memory. Where available, I report and discuss empirical evidence on EC that speaks to these hypotheses. The available empirical evidence is largely in line with the predictions of the DMM. Several predictions, however, have yet to be tested and some findings are ambiguous. While the DMM specifies conditions under which CS-US pairings should lead to a valence change, it does not deny the possibility that other processes might lead to a change in attitude as well. Advantages of the DMM are its foundation on declarative memory research, its applicability for attitude change effects in general, and its suitability for predictions of EC effects in the real world.

Sign in / Sign up

Export Citation Format

Share Document