publication . Preprint . Article . 2012

Relaxed Operational Semantics of Concurrent Programming Languages

Gérard Boudol; Bernard Serpette; Gustavo Petri;
Open Access English
  • Published: 12 Aug 2012
Abstract
We propose a novel, operational framework to formally describe the semantics of concurrent programs running within the context of a relaxed memory model. Our framework features a "temporary store" where the memory operations issued by the threads are recorded, in program order. A memory model then specifies the conditions under which a pending operation from this sequence is allowed to be globally performed, possibly out of order. The memory model also involves a "write grain," accounting for architectures where a thread may read a write that is not yet globally visible. Our formal model is supported by a software simulator, allowing us to run litmus tests in ou...
Subjects
free text keywords: Computer Science - Programming Languages, Computer Science - Logic in Computer Science, Mathematics, QA1-939, Electronic computers. Computer science, QA75.5-76.95, Operational semantics, Litmus, Concurrent computing, Out-of-order execution, Thread (computing), Operational framework, Computer science, Semantics, Memory model, Programming language, computer.software_genre, computer

[1] S. ADVE, H.-J. BOEHM, Memory models: a case for rethinking parallel languages and hardware, CACM Vol. 53 No. 8 () 90-101. doi:10.1145/1787234.1787255

[2] S. ADVE, K. GHARACHORLOO, Shared memory consistency models: a tutorial, IEEE Computer Vol. 29 No. 12 () 66-76. doi:10.1109/2.546611

[3] S. ADVE, M. D. HILL, doi:10.1145/325096.325100

Abstract
We propose a novel, operational framework to formally describe the semantics of concurrent programs running within the context of a relaxed memory model. Our framework features a "temporary store" where the memory operations issued by the threads are recorded, in program order. A memory model then specifies the conditions under which a pending operation from this sequence is allowed to be globally performed, possibly out of order. The memory model also involves a "write grain," accounting for architectures where a thread may read a write that is not yet globally visible. Our formal model is supported by a software simulator, allowing us to run litmus tests in ou...
Subjects
free text keywords: Computer Science - Programming Languages, Computer Science - Logic in Computer Science, Mathematics, QA1-939, Electronic computers. Computer science, QA75.5-76.95, Operational semantics, Litmus, Concurrent computing, Out-of-order execution, Thread (computing), Operational framework, Computer science, Semantics, Memory model, Programming language, computer.software_genre, computer

[1] S. ADVE, H.-J. BOEHM, Memory models: a case for rethinking parallel languages and hardware, CACM Vol. 53 No. 8 () 90-101. doi:10.1145/1787234.1787255

[2] S. ADVE, K. GHARACHORLOO, Shared memory consistency models: a tutorial, IEEE Computer Vol. 29 No. 12 () 66-76. doi:10.1109/2.546611

[3] S. ADVE, M. D. HILL, doi:10.1145/325096.325100

Any information missing or wrong?Report an Issue