Sciweavers

Share
warning: Creating default object from empty value in /var/www/modules/taxonomy/taxonomy.module on line 1416.
CAV
2006
Springer
165views Hardware» more  CAV 2006»
10 years 8 months ago
Bounded Model Checking of Concurrent Data Types on Relaxed Memory Models: A Case Study
Many multithreaded programs employ concurrent data types to safely share data among threads. However, highly-concurrent algorithms for even seemingly simple data types are difficul...
Sebastian Burckhardt, Rajeev Alur, Milo M. K. Mart...
CAV
2010
Springer
187views Hardware» more  CAV 2010»
10 years 8 months ago
Fences in Weak Memory Models
We present a class of relaxed memory models, deļ¬ned in Coq, parameterised by the chosen permitted local reorderings of reads and writes, and the visibility of inter- and intra-pr...
Jade Alglave, Luc Maranget, Susmit Sarkar, Peter S...
CC
2010
Springer
172views System Software» more  CC 2010»
10 years 11 months ago
Verifying Local Transformations on Relaxed Memory Models
The problem of locally transforming or translating programs without altering their semantics is central to the construction of correct compilers. For concurrent shared-memory progr...
Sebastian Burckhardt, Madanlal Musuvathi, Vasu Sin...
ESOP
2010
Springer
11 years 1 months ago
Parameterized Memory Models and Concurrent Separation Logic
Formal reasoning about concurrent programs is usually done with the assumption that the underlying memory model is sequentially consistent, i.e. the execution outcome is equivalen...
Rodrigo Ferreira, Xinyu Feng and Zhong Shao
CAV
2009
Springer
177views Hardware» more  CAV 2009»
11 years 4 months ago
Software Transactional Memory on Relaxed Memory Models
Abstract. Pseudo-code descriptions of STMs assume sequentially consistent program execution and atomicity of high-level STM operations like read, write, and commit. These assumptio...
Rachid Guerraoui, Thomas A. Henzinger, Vasu Singh
books