scholarly journals Verified compilation of C programs with a nominal memory model

2022 ◽  
Vol 6 (POPL) ◽  
pp. 1-31
Author(s):  
Yuting Wang ◽  
Ling Zhang ◽  
Zhong Shao ◽  
Jérémie Koenig
Keyword(s):  
Global Memory ◽  
Memory Model ◽  
Global Constraints ◽  
Concurrent Programs ◽  
Intuitive Reasoning ◽  
Contextual Memory ◽  
Memory Space ◽  
C Programs ◽  
Block Based ◽  
Verification Techniques

Memory models play an important role in verified compilation of imperative programming languages. A representative one is the block-based memory model of CompCert---the state-of-the-art verified C compiler. Despite its success, the abstraction over memory space provided by CompCert's memory model is still primitive and inflexible. In essence, it uses a fixed representation for identifying memory blocks in a global memory space and uses a globally shared state for distinguishing between used and unused blocks. Therefore, any reasoning about memory must work uniformly for the global memory; it is impossible to individually reason about different sub-regions of memory (i.e., the stack and global definitions). This not only incurs unnecessary complexity in compiler verification, but also poses significant difficulty for supporting verified compilation of open or concurrent programs which need to work with contextual memory, as manifested in many previous extensions of CompCert. To remove the above limitations, we propose an enhancement to the block-based memory model based on nominal techniques; we call it the nominal memory model. By adopting the key concepts of nominal techniques such as atomic names and supports to model the memory space, we are able to 1) generalize the representation of memory blocks to any types satisfying the properties of atomic names and 2) remove the global constraints for managing memory blocks, enabling flexible memory structures for open and concurrent programs. To demonstrate the effectiveness of the nominal memory model, we develop a series of extensions of CompCert based on it. These extensions show that the nominal memory model 1) supports a general framework for verified compilation of C programs, 2) enables intuitive reasoning of compiler transformations on partial memory; and 3) enables modular reasoning about programs working with contextual memory. We also demonstrate that these extensions require limited changes to the original CompCert, making the verification techniques based on the nominal memory model easy to adopt.

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 SecRSL: security separation logic for C11 release-acquire concurrency

2021 ◽  
Vol 5 (OOPSLA) ◽  
pp. 1-26
Author(s):  
Pengbo Yan ◽  
Toby Murray
Keyword(s):  
Information Flow ◽  
Separation Logic ◽  
Constant Time ◽  
Memory Model ◽  
C Programs ◽  
Information Flow Security ◽  
Empirical Performance ◽  
Functional Correctness ◽  
Local Reasoning ◽  
High Level

We present Security Relaxed Separation Logic (SecRSL), a separation logic for proving information-flow security of C11 programs in the Release-Acquire fragment with relaxed accesses. SecRSL is the first security logic that (1) supports weak-memory reasoning about programs in a high-level language; (2) inherits separation logic’s virtues of compositional, local reasoning about (3) expressive security policies like value-dependent classification. SecRSL is also, to our knowledge, the first security logic developed over an axiomatic memory model. Thus we also present the first definitions of information-flow security for an axiomatic weak memory model, against which we prove SecRSL sound. SecRSL ensures that programs satisfy a constant-time security guarantee, while being free of undefined behaviour. We apply SecRSL to implement and verify the functional correctness and constant-time security of a range of concurrency primitives, including a spinlock module, a mixed-sensitivity mutex, and multiple synchronous channel implementations. Empirical performance evaluations of the latter demonstrate SecRSL’s power to support the development of secure and performant concurrent C programs.

scholarly journals GenMC: A Model Checker for Weak Memory Models

2021 ◽  
pp. 427-440
Author(s):  
Michalis Kokologiannakis ◽  
Viktor Vafeiadis
Keyword(s):  
Programming Languages ◽  
Error Detection ◽  
State Of The Art ◽  
Memory Models ◽  
Memory Model ◽  
Model Checker ◽  
C Programs ◽  
System Calls ◽  
Detection Capabilities ◽  
Additional Memory

AbstractGenMC is an LLVM-based state-of-the-art stateless model checker for concurrent C/C++ programs. Its modular infrastructure allows it to support complex memory models, such as RC11 and IMM, and makes it easy to extend to support further axiomatic memory models.In this paper, we discuss the overall architecture of the tool and how it can be extended to support additional memory models, programming languages, and/or synchronization primitives. To demonstrate the point, we have extended the tool with support for the Linux kernel memory model (LKMM), synchronization barriers, POSIX I/O system calls, and better error detection capabilities.

scholarly journals Generalized Load Sharing for Homogeneous Networks of Distributed Environment

2008 ◽  
Vol 2008 ◽  
pp. 1-9 ◽  
Author(s):  
A. Satheesh ◽  
K. Vimal Kumar ◽  
S. Krishnaveni
Keyword(s):  
High Performance ◽  
Load Sharing ◽  
Global Memory ◽  
Distributed Environment ◽  
Memory Space ◽  
Remote Execution ◽  
Execution Strategy ◽  
Migration Strategies ◽  
Overall Performance ◽  
Memory Resources

We propose a method for job migration policies by considering effective usage of global memory in addition to CPU load sharing in distributed systems. When a node is identified for lacking sufficient memory space to serve jobs, one or more jobs of the node will be migrated to remote nodes with low memory allocations. If the memory space is sufficiently large, the jobs will be scheduled by a CPU-based load sharing policy. Following the principle of sharing both CPU and memory resources, we present several load sharing alternatives. Our objective is to reduce the number of page faults caused by unbalanced memory allocations for jobs among distributed nodes, so that overall performance of a distributed system can be significantly improved. We have conducted trace-driven simulations to compare CPU-based load sharing policies with our policies. We show that our load sharing policies not only improve performance of memory bound jobs, but also maintain the same load sharing quality as the CPU-based policies for CPU-bound jobs. Regarding remote execution and preemptive migration strategies, our experiments indicate that a strategy selection in load sharing is dependent on the amount of memory demand of jobs, remote execution is more effective for memory-bound jobs, and preemptive migration is more effective for CPU-bound jobs. Our CPU-memory-based policy using either high performance or high throughput approach and using the remote execution strategy performs the best for both CPU-bound and memory-bound job in homogeneous networks of distributed environment.

Sign in / Sign up

Export Citation Format

Share Document