Formalisation of a New Weak Semantics for AuDaLa
摘要
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.