The benefits of fast computer systems are clear - improving performance allows more sophisticated applications to be developed. Speed-up via higher processor clock speeds, however, reached a physical upper limit in the early 2000s, with power-dissipation becoming a major issue. Hardware designers have therefore switched to multicore processors with fixed clock speeds, where speed-up is achieved by including several cores in a single processor. Multicore processors are now pervasive in all aspects of computing, from cluster servers and desktops to low-power mobile devices.
A multicore processor efficiently executes concurrent programs comprising multiple threads by allowing several computations to take place simultaneously in the different cores. These threads communicate via synchronised access and modification of shared resources stored in shared memory. While some problems (coined embarrassingly parallel problems) are naturally able to take advantage of multicore computing, the majority require clever management of thread synchronisation that is difficult to achieve. Moreover, modern architectures have forced programmers to understand intricate details of the hardware/software interface in addition to concurrency issues within the programs they develop.
Within a multicore processor, each processing core has access to a local buffer that acts as a temporary cache - any writes stored in a local buffer are not visible to other cores until the buffer is flushed. For efficiency reasons, multicore architectures implement so-called relaxed-memory models, where read and write events within a single thread may take effect in shared memory out-of-order, leading to behaviours that may not be expected by a programmer. Restoring correctness requires manual introduction of "fence" instructions in a program's code, which is a non-trivial task - under-fencing leads to incorrect behaviours, while overfencing leads to inefficient programs. Therefore, as Shavit states, "The advent of multicore processors as the standard computing platform will force major changes in software design." There is a large international effort in both academia and industry to make better use of multicore processing, ranging from new foundational and theoretical underpinnings to the development of novel abstractions, tool support, engineering paradigms, etc.
In this project, we aim to simplify system development via practical solutions that are highly performant (to increase efficiency), verifiably correct (to ensure dependability) and cope with relaxed-memory models (as used by modern hardware). In particular, we develop efficient "concurrent objects" that provide abstractions from the low-level hardware interface and manage thread synchronisation on behalf of a programmer. Concurrent objects are to ultimately become part of a programming language library - some languages e.g., Java already offer basic concurrent objects as part of their standard library - hence are highly applicable.
The objects we deliver will take advantage of relaxed memory models. Here, it is well known that correctness conditions that are too strict (e.g., linearizability) are themselves becoming a barrier to efficiency.
We therefore begin by developing new theoretical foundations in the form of relaxed correctness conditions that match relaxed memory models. A hierachy of different conditions will be developed, enabling one to easily determine the relative strengths of each condition. These conditions will be linked to a contextual notion of refinement to provide a basis for substitutability in client programs. This provides a basis for more efficient, verifiably correct, concurrent objects for relaxed memory models. We will focus on developing concurrent data structures (e.g., stacks, queues, deques) for the TSO memory model. Their verification will be mechanised in the KIV theorem prover to eliminate human error in verification, which in turn improves dependability.
|