Catálogo de publicaciones - libros

(SVP) is a fine-grain, thread-based model of concurrent program composition developed and used at the University of Amsterdam as a basis for designing and programming many-core chips. Its design goal was to support dynamic concurrency and hence support self-adaptive systems within the AETHER collaborative European project. It provides an effective solution for programming chip multiprocessor systems [1,2,3]. In this paper, we take thread algebra [4], a semantics for recent object-oriented programming languages such as C# and Java, as a theoretical framework to the verification and evaluation of SVP. We show how a SVP program behavior can be determined in , an extension of thread algebra with the features of SVP, and prove that SVP programs satisfy the determinism property, i.e. the programs always give the same result, a key property of the sequential paradigm that SVP will replace.

To facilitate the construction of concurrent programs based on progress requirements, we study an integration of the Owicki/Gries theory with UNITY’s leads-to relation. In particular we investigate a set of calculational rules for leads-to, and we study the composition of programs regarding their effect on progress. Apart from parallel composition, we consider the less familiar notion of weak sequential composition. Our techniques are illustrated on two network initialisation protocols that are related to the protocol standard IEEE 1394.