MSc Presentation: Model Checking LLVM IR using LTSmin

When: Dec. 20, 2013, 16:00-17:30

Where: Carre 2H

Who: Freark van der Berg

Advancements in computer architectures have resulted in an exponential increase in the speed of processors and memory capacity. However, memory latencies have not improved to the same extent, thus access times are increasingly limiting peak performance. To address this, several layers of cache are added to computer architectures to speed up apparent memory access and instruction are reordered to maximize memory bandwidth. 

This worked fine for single-processor systems, but because of physical limits, modern computer architectures gain performance by adding more processors instead of increasing the clock speed. In multi-processor systems, the cache and instruction reordering make communication complex, because reads and writes of one processor may be observed in a different orders by different processors. To mitigate this, some computer architectures add complex hardware at the cost of performance, power requirements and die size. Other architectures employ a relaxed memory model and add synchronization instructions, memory barriers, to the instruction set. This means the software has to deal with the complexity. By placing memory barriers, an ordering on reads and writes can be enforced, causing processors to synchronize.

However, memory barriers are expensive instructions and need only to be placed where absolutely needed if performance is of importance. To this end, we present our tool, llmc. The target of llmc is concurrent programs written in LLVM IR, an intermediate representation language with numerous front-ends, e.g. for C, C , Java, .NET, and Erlang. Using the model checker LTSmin, we explore the state space of these programs in search of assertion violations and report if the cause is a missing memory barrier.