The Autonomous Data Language -- Concepts, Design and Formal Verification

TL;DR

The paper introduces the data-autonomous paradigm and AuDaLa, a language where data elements execute computations under a global schedule, decoupling computation from processors. It formalizes AuDaLa with a rigorous type system and a stack-based operational semantics, enabling formal verification of parallel programs and proving properties like safety and determinism under race-free conditions. The authors demonstrate the framework through several standard parallel algorithms (spanning tree, sorting, 3SUM) and provide proofs of correctness for selected programs (prefix sum, sort2), illustrating modular, contract-based verification. They also discuss related work, practical considerations (weak memory semantics, CUDA backend), and avenues for future enhancements including inheritance, packaging, debugging, and mechanized proofs. Overall, the work positions AuDaLa as a rigorous, verifiable data-centric alternative to traditional thread- and task-based parallelism with potential practical compilers and implementations.

Abstract

Nowadays, the main advances in computational power are due to parallelism. However, most parallel languages have been designed with a focus on processors and threads. This makes dealing with data and memory in programs hard, which distances the implementation from its original algorithm. We propose a new paradigm for parallel programming, the data-autonomous paradigm, where computation is performed by autonomous data elements. Programs in this paradigm are focused on making the data collaborate in a highly parallel fashion. We furthermore present AuDaLa, the first data autonomous programming language, and provide a full formalisation that includes a type system and operational semantics. Programming in AuDaLa is very natural, as illustrated by examples, albeit in a style very different from sequential and contemporary parallel programming. Additionally, it lends itself for the formal verification of parallel programs, which we demonstrate.

Figures (7)

• Figure 1: Approximate placement of related work on an axis from process-focused (left) to data-focused (right) paradigms.
• Figure 2: The three main components of an AuDaLa program.
• Figure 3: Execution of Prefix Sum on a small list. The left side of a list element holds the parameter val, while the right side holds the parameter auxval. The parameter prev is shown as unmarked black arrows, while the parameter auxprev is shown as unmarked grey arrows.
• Figure 4: Execution of Listing \ref{['ex: BFS']} on a small graph. Every Edge newly considered in the current step is grey. Considered Edges stay considered, but stable. The dotted arrows denote the possible new values for t.in of a target node $t$. Note that the Edge from $c$ to $d$ wins the race condition to the reference $d.in$.
• Figure 5: Execution of Listing \ref{['ex: Sort']} on a small list. The parameters next, newNext and comp are shown as black, grey and dashed unmarked arrows respectively, and the null-references for newNext and comp are not shown. The nodes corresponding to ListElems contain the value of parameter val.

Theorems & Definitions (77)

• definition 1: AuDaLa well-formedness
• definition 2: Commands
• definition 3: Interpretation function
• definition 4: Struct instance
• definition 5: State
• definition 6: Null-instances
• definition 7: Initial state
• definition 8: Operational semantics
• definition 9: Reference Notation
• definition 10: AuDaLa Execution