Designing GALS software systems using libraries and run-time OS support

Abstract

With the increasing use of multicore and distributed computing platforms, software systems are becoming more and more complex and as such require tremendous design effort. They are also very difficult to debug and guarantee for correct functionality. In the case of embedded systems, ideally, software development could proceed in parallel with the development of the target hardware if this is not known in advance. This thesis addresses complex software systems development which can be underpinned by formal models of computation and which use some kind of operating system to abstract the hardware platform from system developers. Two specific models of computation, synchronous reactive and asynchronous, combined into a Globally Asynchronous Locally Synchronous (GALS) model are used as the underlying formal model of the target systems. A set of tools to implement the GALS model in traditional programming languages, C and C++, is used to enable re-use of huge legacy codes. The tools consist of libraries and run-time support that allow the design of two types of GALS systems for the range of target platforms: (1) static systems with a fixed number of concurrent processes and (2) dynamic GALS (DGALS) systems where the number of processes varies during system life. The implemented libraries and run-time support depend only minimally on the operating system, since they use a very primitive synchronization mechanism in the form of semaphores, and are ported to a number of non-real-time and real-time operating systems with identical application programming interface (API). A specific version of API is developed for the development of static GALS systems in system-level design language SYSTEMC, which allows system designers to model both hardware and software within the same system model, thus developing software before the actual hardware is available. The developed APIs are in compliance with the GALS model of computation (MoC), opening the possibilities for formal verification of designs or their parts, or of the use of the API in conjunction with programming languages based on GALS MoC.