Export to

• Google Calendar
• iCalendar file
• hCalendar markup
  <div class="vevent h-event"> <h1 class="summary p-name">Galois Tech Talk (3/3 next week!): On deadlock verification in micro-architectural models of communication fabrics.</h1> <div class='date'><time class="dtstart dt-start" title="2012-01-12T10:30:00" datetime="2012-01-12T10:30:00">Thursday, January 12, 2012 from 10:30</time>–<time class="dtend dt-end" title="2012-01-12T11:30:00" datetime="2012-01-12T11:30:00">11:30am</time></div> <div class="location vcard p-location h-card"> <a class="url" href='http://calagator.org/venues/202390439'><span class='fn org p-name'>Galois, Inc</span></a> <div class="adr p-adr h-adr"> <div class="street-address p-street-address">421 SW 6th Ave. Suite 300</div> <span class="locality p-locality">Portland</span> , <span class="region p-region">OR</span> <span class="postal-code p-postal-code">97204</span> <div class="country-name p-country-name">US</div> (<a href='https://maps.google.com/maps?q=421%20SW%206th%20Ave.%20Suite%20300,%20Portland%20OR%2097204%20US'>map</a>) </div> </div> <div class="description p-description"> <p>Presented by Julien Schmaltz.</p> <p>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.</p> </div> <h3>Links</h3> <ul> <li><a class="url u-url" href="https://corp.galois.com/blog/2012/1/5/galois-tech-talk-33-next-week-on-deadlock-verification-in-mi.html">Website</a></li> </ul> </div>