CTIT University of Twente
Research Business & Innovation About CTIT Research Calls Looking for a job? Intranet

MADRID: Multicore Decision Diagram

Project Number: 612.001.101
Project Manager: Prof. dr. Jaco C. van de Pol
Faculty of Electrical Engineering, Mathematics and Computer Science
Tel.: +31-53-4893017
Email: j.c.vandepol@utwente.nl

Project website: MaDriD

Summary

The goal of the MaDriD project is to design, analyze, build and measure multi-core algorithms for Binary Decision Diagrams. BDDs are perhaps the most fundamental data structure in symbolic computing. Applications in hardware and software verification need prohibitively large BDDs, defeating memory and time limitations. Previous attempts targeted massively parallel supercomputers, networks of workstations or external disks, with only disappointing speedup.

Those solutions are not applicable to modern multi-core architectures, which have a number of independent processors accessing a large shared memory. Multi-core processors share many resources, like the memory bus and hardware caches. Unfortunately, BDD algorithms are extremely memory-intensive; memory access is irregular and the time required by the basic operations varies from constant to quadratic. Therefore, developing multi-core BDD algorithms whose performance scales proportional to the number of processors, is a difficult challenge.

Our long term goal is to investigate how to design high-performing software for multi-core compueters, and how to analyze correctness and performance at design time, program level and runtime.

Correctness proofs for parallel programs are notoriously hard due to concurrency; our case is beyond what is currently feasible. For performance reasons we will rely on mostly lock-free synchronization, allowing benign data races. So we must also take into account instruction reordering due to optimizations by the compiler and the CPU.

Performance prediction is hard due to the effects of irregular memory access, cache misses, false sharing and lock contention. We intend to do extensive measurements, on which self-adaptation mechanisms can be built."

Project duration: 1-5-2012 / 1-5-2016
Project budget: 208.5 k-€ funding
Number of person/months: 48 person months
Involved groups: Formal Methods & Tools group
CTIT Research Centre:
Centre for Safety and Security in Smart Societies (CS.4)