| dc.description.abstract | Does your program do what it is supposed to be doing? Without running the program
providing an answer to this question is much harder if the language does not support
static type checking. Of course, even if compile-time checks are in place only certain
errors will be detected: compilers can only second-guess the programmer’s intention.
But, type based techniques go a long way in assisting programmers to detect errors
in their computations earlier on. The question if a program behaves correctly is even
harder to answer if the program consists of several parts that execute concurrently and
need to communicate with each other. Compilers of standard programming languages
are typically unable to infer information about how the parts of a concurrent program
interact with each other, especially where explicit threading or message passing techniques
are used. Hence, correctness guarantees are often conspicuously absent.
Concurrency management in an application is a complex problem. However, it is
largely orthogonal to the actual computational functionality that a program realises.
Because of this orthogonality, the problem can be considered in isolation. The largest
possible separation between concurrency and functionality is achieved if a dedicated
language is used for concurrency management, i.e. an additional program manages
the concurrent execution and interaction of the computational tasks of the original
program. Such an approach does not only help programmers to focus on the core
functionality and on the exploitation of concurrency independently, it also allows for
a specialised analysis mechanism geared towards concurrency-related properties.
This dissertation shows how an approach that completely decouples coordination
from computation is a very supportive substrate for inferring static guarantees of the
correctness of concurrent programs. Programs are described as streaming networks
connecting independent components that implement the computations of the program,
where the network describes the dependencies and interactions between components.
A coordination program only requires an abstract notion of computation
inside the components and may therefore be used as a generic and reusable design
pattern for coordination. A type-based inference and checking mechanism analyses
such streaming networks and provides comprehensive guarantees of the consistency
and behaviour of coordination programs.
Concrete implementations of components are deliberately left out of the scope of
coordination programs: Components may be implemented in an external language,
for example C, to provide the desired computational functionality. Based on this separation,
a concise semantic framework allows for step-wise interpretation of coordination
programs without requiring concrete implementations of their components. The
framework also provides clear guidance for the implementation of the language. One
such implementation is presented and hands-on examples demonstrate how the language
is used in practice. | en_US |
