AbstractMulti-core processors have become ubiquitous in modern hardware. However, efficiently exploit- ing the parallelism offered by these architectures still remains a challenge. Concurrency models allow the programmer to structure his code in logically separated concurrent tasks. How the different operations are structured into logically separated concurrent tasks and how these differ- ent tasks are synchronised heavily depends on the concurrency model that is used. Concurrency models come in a wide array of flavours and each of them is well suited for expressing a particular type of concurrency. The starting hypothesis of this thesis is that application developers can benefit from combining different concurrency models to parallelise the different parts of their application.
This thesis investigates the combination of two concurrency models, namely the actor model and software transactional memory. Both models offer certain semantic guarantees that allow programmers to write lock-free code. However, the former model does not allow shared mutable state by design which is one of its strengths but limits expresiveness. This thesis investigates whether it is possible to combine the actor model with software transactional memory into a conglomerate model that still satisfies the semantic properties that both models guarantee when used in isolation, and does not introduce additional liveness or safety issues.
We provide a unified list of semantic properties of both software transactional memory and actor languages which will form the correctness criteria for our result. The violation of these properties by the ad hoc combination is illustrated by means of several examples. For both models a library is implemented in Clojure as an experimental platform.
We compose a novel formal semantics that show that the actor model can be safely combined with software transactional memory while still ensuring the semantic properties that each model guarantees if used in isolation. As a proof of concept we provide an implementation of the formal semantics in Clojure under the name Actransors which is comprised of a modified version of the two aforementioned libraries.
We validate our approach by translating an existing Clojure application into a version that uses Actransors which results in an equivalent application with added expressivity. Finally we informally prove that the semantic properties of both models remain intact.
|Date of Award||14 Jun 2015|
|Supervisor||Wolfgang De Meuter (Promotor), Joeri De Koster (Promotor) & Janwillem Swalens (Promotor)|