A Denotational Semantics for SPARC TSO
The SPARC TSO weak memory model is defined axiomatically, with a non-compositional formulation that makes modular reasoning about programs difficult. Our denotational approach uses pomsets to provide a compositional semantics capturing exactly the behaviours permitted by SPARC TSO. It uses buffered...
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Logical Methods in Computer Science e.V.
2019-05-01
|
| Series: | Logical Methods in Computer Science |
| Subjects: | |
| Online Access: | https://lmcs.episciences.org/4051/pdf |
| _version_ | 1797268563697860608 |
|---|---|
| author | Ryan Kavanagh Stephen Brookes |
| author_facet | Ryan Kavanagh Stephen Brookes |
| author_sort | Ryan Kavanagh |
| collection | DOAJ |
| description | The SPARC TSO weak memory model is defined axiomatically, with a
non-compositional formulation that makes modular reasoning about programs
difficult. Our denotational approach uses pomsets to provide a compositional
semantics capturing exactly the behaviours permitted by SPARC TSO. It uses
buffered states and an inductive definition of execution to assign an
input-output meaning to pomsets. We show that our denotational account is sound
and complete relative to the axiomatic account, that is, that it captures
exactly the behaviours permitted by the axiomatic account. Our compositional
approach facilitates the study of SPARC TSO and supports modular analysis of
program behaviour. |
| first_indexed | 2024-04-25T01:34:28Z |
| format | Article |
| id | doaj.art-67d96cf8752a42a69ad3d5185994dd0a |
| institution | Directory Open Access Journal |
| issn | 1860-5974 |
| language | English |
| last_indexed | 2024-04-25T01:34:28Z |
| publishDate | 2019-05-01 |
| publisher | Logical Methods in Computer Science e.V. |
| record_format | Article |
| series | Logical Methods in Computer Science |
| spelling | doaj.art-67d96cf8752a42a69ad3d5185994dd0a2024-03-08T10:27:59ZengLogical Methods in Computer Science e.V.Logical Methods in Computer Science1860-59742019-05-01Volume 15, Issue 210.23638/LMCS-15(2:10)20194051A Denotational Semantics for SPARC TSORyan Kavanaghhttps://orcid.org/0000-0001-9497-4276Stephen BrookesThe SPARC TSO weak memory model is defined axiomatically, with a non-compositional formulation that makes modular reasoning about programs difficult. Our denotational approach uses pomsets to provide a compositional semantics capturing exactly the behaviours permitted by SPARC TSO. It uses buffered states and an inductive definition of execution to assign an input-output meaning to pomsets. We show that our denotational account is sound and complete relative to the axiomatic account, that is, that it captures exactly the behaviours permitted by the axiomatic account. Our compositional approach facilitates the study of SPARC TSO and supports modular analysis of program behaviour.https://lmcs.episciences.org/4051/pdfcomputer science - programming languagesf.3.2 |
| spellingShingle | Ryan Kavanagh Stephen Brookes A Denotational Semantics for SPARC TSO Logical Methods in Computer Science computer science - programming languages f.3.2 |
| title | A Denotational Semantics for SPARC TSO |
| title_full | A Denotational Semantics for SPARC TSO |
| title_fullStr | A Denotational Semantics for SPARC TSO |
| title_full_unstemmed | A Denotational Semantics for SPARC TSO |
| title_short | A Denotational Semantics for SPARC TSO |
| title_sort | denotational semantics for sparc tso |
| topic | computer science - programming languages f.3.2 |
| url | https://lmcs.episciences.org/4051/pdf |
| work_keys_str_mv | AT ryankavanagh adenotationalsemanticsforsparctso AT stephenbrookes adenotationalsemanticsforsparctso AT ryankavanagh denotationalsemanticsforsparctso AT stephenbrookes denotationalsemanticsforsparctso |