Formalisation of a New Weak Semantics for AuDaLa

Gijs P. Leemrijse; Tom T.P. Franken; Thomas Neele

doi:10.1007/978-3-031-78750-8_5

Formalisation of a New Weak Semantics for AuDaLa

Gijs P. Leemrijse
, Tom T.P. Franken
, Thomas Neele (Corresponding author)

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

1 Citation (Scopus)

47 Downloads (Pure)

Abstract

The Autonomous Data Language (AuDaLa) is a recently introduced programming language and is supported by an operational semantics. This work presents a new operational semantics for AuDaLa with relaxed memory consistency and incoherent memory, with the goal of allowing more compiler optimisations. We show that both semantics are equivalent under the absence of read/write conflicts. Furthermore, we translate our operational semantics into an axiomatic memory consistency model and show how the memory operations of our semantics can be mapped onto the NVIDIA PTX virtual ISA.

Original language	English
Title of host publication	Automated Technology for Verification and Analysis
Subtitle of host publication	22nd International Symposium, ATVA 2024, Kyoto, Japan, October 21–25, 2024, Proceedings, Part II
Editors	S. Akshay, Aina Niemetz, Sriram Sankaranarayanan
Place of Publication	Cham
Publisher	Springer
Pages	93-116
Number of pages	24
ISBN (Electronic)	978-3-031-78750-8
ISBN (Print)	978-3-031-78749-2
DOIs	https://doi.org/10.1007/978-3-031-78750-8_5
Publication status	Published - 12 Feb 2025
Event	22nd International Symposium on Automated Technology for Verification and Analysis, ATVA 2024 - Kyoto, Japan Duration: 21 Oct 2024 → 25 Oct 2024

Publication series

Name	Lecture Notes in Computer Science (LNCS)
Volume	15055
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	22nd International Symposium on Automated Technology for Verification and Analysis, ATVA 2024
Country/Territory	Japan
City	Kyoto
Period	21/10/24 → 25/10/24

Access to Document

10.1007/978-3-031-78750-8_5

pdfFinal published version, 849 KBLicence: TAVERNE

Cite this

Leemrijse, G. P., Franken, T. T. P., & Neele, T. (2025). Formalisation of a New Weak Semantics for AuDaLa. In S. Akshay, A. Niemetz, & S. Sankaranarayanan (Eds.), Automated Technology for Verification and Analysis: 22nd International Symposium, ATVA 2024, Kyoto, Japan, October 21–25, 2024, Proceedings, Part II (pp. 93-116). (Lecture Notes in Computer Science (LNCS); Vol. 15055). Springer. https://doi.org/10.1007/978-3-031-78750-8_5

Leemrijse, Gijs P. ; Franken, Tom T.P. ; Neele, Thomas. / Formalisation of a New Weak Semantics for AuDaLa. Automated Technology for Verification and Analysis: 22nd International Symposium, ATVA 2024, Kyoto, Japan, October 21–25, 2024, Proceedings, Part II. editor / S. Akshay ; Aina Niemetz ; Sriram Sankaranarayanan. Cham : Springer, 2025. pp. 93-116 (Lecture Notes in Computer Science (LNCS)).

@inproceedings{b9bad359abbe451ea259c433bfcee61d,

title = "Formalisation of a New Weak Semantics for AuDaLa",

abstract = "The Autonomous Data Language (AuDaLa) is a recently introduced programming language and is supported by an operational semantics. This work presents a new operational semantics for AuDaLa with relaxed memory consistency and incoherent memory, with the goal of allowing more compiler optimisations. We show that both semantics are equivalent under the absence of read/write conflicts. Furthermore, we translate our operational semantics into an axiomatic memory consistency model and show how the memory operations of our semantics can be mapped onto the NVIDIA PTX virtual ISA.",

author = "Leemrijse, \{Gijs P.\} and Franken, \{Tom T.P.\} and Thomas Neele",

year = "2025",

month = feb,

day = "12",

doi = "10.1007/978-3-031-78750-8\_5",

language = "English",

isbn = "978-3-031-78749-2",

series = "Lecture Notes in Computer Science (LNCS)",

publisher = "Springer",

pages = "93--116",

editor = "S. Akshay and Aina Niemetz and Sriram Sankaranarayanan",

booktitle = "Automated Technology for Verification and Analysis",

address = "Germany",

note = "22nd International Symposium on Automated Technology for Verification and Analysis, ATVA 2024 ; Conference date: 21-10-2024 Through 25-10-2024",

}

Leemrijse, GP, Franken, TTP & Neele, T 2025, Formalisation of a New Weak Semantics for AuDaLa. in S Akshay, A Niemetz & S Sankaranarayanan (eds), Automated Technology for Verification and Analysis: 22nd International Symposium, ATVA 2024, Kyoto, Japan, October 21–25, 2024, Proceedings, Part II. Lecture Notes in Computer Science (LNCS), vol. 15055, Springer, Cham, pp. 93-116, 22nd International Symposium on Automated Technology for Verification and Analysis, ATVA 2024, Kyoto, Japan, 21/10/24. https://doi.org/10.1007/978-3-031-78750-8_5

Formalisation of a New Weak Semantics for AuDaLa. / Leemrijse, Gijs P.; Franken, Tom T.P.; Neele, Thomas (Corresponding author).
Automated Technology for Verification and Analysis: 22nd International Symposium, ATVA 2024, Kyoto, Japan, October 21–25, 2024, Proceedings, Part II. ed. / S. Akshay; Aina Niemetz; Sriram Sankaranarayanan. Cham: Springer, 2025. p. 93-116 (Lecture Notes in Computer Science (LNCS); Vol. 15055).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - Formalisation of a New Weak Semantics for AuDaLa

AU - Leemrijse, Gijs P.

AU - Franken, Tom T.P.

AU - Neele, Thomas

PY - 2025/2/12

Y1 - 2025/2/12

N2 - The Autonomous Data Language (AuDaLa) is a recently introduced programming language and is supported by an operational semantics. This work presents a new operational semantics for AuDaLa with relaxed memory consistency and incoherent memory, with the goal of allowing more compiler optimisations. We show that both semantics are equivalent under the absence of read/write conflicts. Furthermore, we translate our operational semantics into an axiomatic memory consistency model and show how the memory operations of our semantics can be mapped onto the NVIDIA PTX virtual ISA.

AB - The Autonomous Data Language (AuDaLa) is a recently introduced programming language and is supported by an operational semantics. This work presents a new operational semantics for AuDaLa with relaxed memory consistency and incoherent memory, with the goal of allowing more compiler optimisations. We show that both semantics are equivalent under the absence of read/write conflicts. Furthermore, we translate our operational semantics into an axiomatic memory consistency model and show how the memory operations of our semantics can be mapped onto the NVIDIA PTX virtual ISA.

UR - https://www.scopus.com/pages/publications/85219209328

U2 - 10.1007/978-3-031-78750-8_5

DO - 10.1007/978-3-031-78750-8_5

M3 - Conference contribution

AN - SCOPUS:85219209328

SN - 978-3-031-78749-2

T3 - Lecture Notes in Computer Science (LNCS)

SP - 93

EP - 116

BT - Automated Technology for Verification and Analysis

A2 - Akshay, S.

A2 - Niemetz, Aina

A2 - Sankaranarayanan, Sriram

PB - Springer

CY - Cham

T2 - 22nd International Symposium on Automated Technology for Verification and Analysis, ATVA 2024

Y2 - 21 October 2024 through 25 October 2024

ER -

Leemrijse GP, Franken TTP , Neele T. Formalisation of a New Weak Semantics for AuDaLa. In Akshay S, Niemetz A, Sankaranarayanan S, editors, Automated Technology for Verification and Analysis: 22nd International Symposium, ATVA 2024, Kyoto, Japan, October 21–25, 2024, Proceedings, Part II. Cham: Springer. 2025. p. 93-116. (Lecture Notes in Computer Science (LNCS)). doi: 10.1007/978-3-031-78750-8_5