|
Change #12189
2012-01-05
17:24:27
|
create
Calagator::Event
1250461808
Galois Tech Talk (3/3 next week!): On deadlock verification in micro-architectural models of communication fabrics.
Roll back
| description |
nil |
→ |
Presented by Julien Schmaltz.
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. |
| end_time |
nil |
→ |
2012-01-12 11:30:00 -0800 |
| id |
nil |
→ |
1250461808 |
| start_time |
nil |
→ |
2012-01-12 10:30:00 -0800 |
| title |
nil |
→ |
Galois Tech Talk (3/3 next week!): On deadlock verification in micro-architectural models of communication fabrics. |
| url |
nil |
→ |
https://corp.galois.com/blog/2012/1/5/galois-tech-talk-33-next-week-on-deadlock-verification-in-mi.html |
| venue_id |
nil |
→ |
202390439 |
|