Nuno P. Lopes
This thesis presents DAHL, a programming environment for the development of distributed systems. DAHL provides a high-level language that is specialized for the implementation of distributed systems, and a stable and high-performance runtime that can efficiently execute DAHL programs in a production environment.
The DAHL language is declarative, event-triggered and rule based, which enables concise, albeit clear, implementations of distributed applications. The DAHL language features the usual control-flow statements, expressive data types, as well as a set of network and security related built-in predicates.
State-of-the-art languages to implement distributed systems include Mace, which is based on C++ and thus lacks aptitude for formal verification, and P2, which is based on Datalog, a query language that is not expressive enough to implement interesting applications. Moreover, the current P2 implementation is not efficient enough for non-purely network bound applications.
DAHL combines the performance and expressiveness of Mace with the succinctness of P2 to create a better and practical programming environment for the development of distributed applications.
To demonstrate the power of DAHL, we implemented several applications of different representative categories. This thesis presents two of them: Chord, a distributed hash table, which is a network driven protocol, and D'ARMC, a distributed software model checker that is CPU-bound.
N. P. Lopes. Practical Executable Specifications for Distributed Systems. Master thesis, Instituto Superior Técnico, Oct. 2009.
@mastersthesis{Lopes-mscthesis,
title = {Practical Executable Specifications for Distributed Systems},
author = {Nuno P. Lopes},
school = {Instituto Superior T\'{e}cnico},
month = oct,
year = 2009
}