A Parallel Programming Perspective – Designing AuDaLa and AuDaLogic

These days, an important avenue for performance optimization of computer programs is parallelism, where multiple processes work together to execute a single program at the same time. As multiple processes are involved, parallel programming not only requires the programmer to account for the local behaviour of every process, but also for the simultaneous behaviour of the processes as a whole. This makes it harder to not only design and implement parallel programs, but also to prove parallel programs correct. The complexity of current languages and frameworks used for parallel programming further worsens these issues.

In this thesis, we introduce the data-autonomous paradigm. As opposed to more conventional parallel programming, where processes manipulate data, in this paradigm, data elements execute their own code during program execution. Following this paradigm, we create the parallel programming language AuDaLa, the Autonomous Data Language. We claim that this language is understandable and feasible in practice, we show that the language has a compact but complete semantics and we demonstrate that the language is verifiable in practice. For this last point we design AuDaLogic, a proof system made for AuDaLa and based on Separation Logic, and prove AuDaLogic sound.