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)