Galois is pleased to host the following tech talk.
These talks are open to the interested public–please join us!
(There is no need to pre-register for the talk.)
Please note the unusual time for this talk, it is on Thursday,
12 January 2012
title:
On deadlock verification in micro-architectural models of communication fabrics.
speaker:
Julien Schmaltz
time:
Thursday, 12 January 2012, 10:30am
location:
Galois Inc.
421 SW 6th Ave. Suite 300,
Portland, OR, USA
(3rd floor of the Commonwealth building)
abstract:
Communication fabrics constitute an important challenge for the design and verification of multicore architectures. To enable their formal analysis, micro-architectural models have been proposed as an efficient abstraction capturing the high-level structure of designs. Micro-architectural models also include a representation of the protocols using the communication fabrics. This combination of different aspects in a single model is crucial for deadlock verification. Deadlocks emerge or are prevented in this combination: a system with a deadlock-free communication network combined with a deadlock-free protocol may have deadlocks or a system with a network with deadlocks combined with a deadlock-free protocol may be deadlock-free. This combination also makes the verification problem more complicated. We will present an algorithm for efficient deadlock verification in micro-architectural models. We will discuss the limitations of this approach and point to future research direction. An important future application of our methodology is the verification of cache coherency at the level of micro-architectures.
bio:
Dr. Schmaltz is assistant professor at the Open University of the Netherlands. He is also affiliated with the Digital Security group at the Radboud University Nijmegen. He obtained a PhD from the University of Grenoble in 2006. Before joining the Open University he was a postdoctoral researcher at the University of Saarland (Germany), the Radboud University Nijmegen, and the Embedded System Institute in Eindhoven (The Netherlands). During his PhD, he visited the University of Texas at Austin. His research currently focuses on the use of formal methods in the verification of on-chip communication architectures. His general research interests include the application of formal methods in security, certification, software engineering, hardware design, and model-based testing. He co-authored more than 40 publications. In 2011, he co-chaired the second international conference on Interactive Theorem Proving and the 10th edition of the international workshop on the ACL2 Theorem Prover and its Applications.