The University of Southampton

Verifying Shared Memory Communication for Low-Power Multi-core SoCs

Date:
2009-
Themes:
Low-Energy Sustainable Systems, Systems Design, Model-Based Verification, Formal Methods, Low-Energy Sustainable Systems, Low-Energy Sustainable Systems

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/

Primary investigators

  • Fan Lu
  • John Colley

Secondary investigator

Associated research group

  • Electronics and Electrical Engineering
Share this project FacebookGoogle+TwitterWeibo

We use cookies to ensure that we give you the best experience on our website. If you continue without changing your settings, we will assume that you are happy to receive cookies on the University of Southampton website.

×