The advent of low-cost, low-power multi-core systems provides the opportunity to exploit the parallelism offered by such systems. However, even if high-level programming models are provided to exploit this parallelism, it is important that the underlying memory-model supports parallel programming in an efficient way. It is also important that the memory model is rigorously defined to facilitate the proper verification of parallel applications.
The memory model defines behaviours of transactions between the memory and the processor. For a uniprocessor system, microarchitectures like out-of-order execution, speculative execution, forwarding and cache hierarchy could effectively increase the performance of systems. For a multiprocessor system with shared memory, such techniques may easily break the sequential consistency in a multi-thread programme and result in unexpected execution. Therefore, weak memory models introduce barrier (fence) instructions to keep the sequential consistency while maintain the optimized system performance by using those techniques. And the verification of the system becomes an important issue to ensure the system behaviours as expected. However, the verification of weak memory models is inefficient by using simulation-based approach. So the formal method-based verification approach is investigated.
Formal methods are mathematical based technique to model and verify software and hardware systems by using model checking and theorem proving [1]. Event-b is one of formal methods which are based on set theory for system-level modelling and analysis. In Event-b, a chain of refinements is used to represent the system at different abstraction levels. With the support of Rodin platform, the consistency of two levels of refinement could be verified by using automated mathematical proof [2]. This project aims to develop weak memory models formally within multiprocessor shared-memory systems in Event-b and to evaluate performance of systems with weak memory models.
References: [1] Neil Storey, Safety-Critical Computer Systems, Pearson Education Limited, Bath, UK,1996 [2] Event-B,http://www.event-b.org/