Export or edit this event...

Export to

Google Calendar
iCalendar file
hCalendar markup
<div class="vevent h-event"> <h1 class="summary p-name">Galois tech talk: Interrupts in OS code: let’s reason about them. Yes, this means concurrency.</h1> <div class='date'><time class="dtstart dt-start" title="2016-05-04T11:00:00" datetime="2016-05-04T11:00:00">Wednesday, May 4, 2016 from 11am</time>–<time class="dtend dt-end" title="2016-05-04T12:00:00" datetime="2016-05-04T12:00:00">noon</time></div> <div class="location vcard p-location h-card"> <a class="url" href='http://calagator.org/venues/202394717'><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 Ste 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%20Ste%20300,%20Portland%20OR%2097204%20US'>map</a>) </div> </div> <div class="description p-description"> <h2>abstract:</h2> <p>Existing modeled and verified operating systems (OS’s) typically run on uniprocessor platforms and run with interrupts mostly disabled. This makes formal reasoning more tractable: execution is mostly sequential. The eChronos OS is a real-time OS used in tightly constrained devices, running on (uniprocessor) embedded micro-controllers. It is used in the DARPA-funded HACMS program, where it runs the flight control software of a high-assurance quadcopter. To provide low latency, the eChronos OS runs with interrupts enabled and provides a preemptive scheduler. In terms of verification, this means that concurrency reasoning is required, which significantly increases the complexity: application and OS instructions may be interleaved with interrupt handler instructions.</p> <p>In our work we explicitly model the effect of interrupts and their handling by the hardware and OS. We provide a general formal model of the interleaving between OS code, application code and interrupt handlers. We then instantiate this model to formalise the scheduling behavior of the eChronos OS, and prove the main scheduler property: the running task is always the highest-priority runnable task.</p> <h2>bio:</h2> <p>June Andronick is a Senior Researcher at Data61|CSIRO (formerly NICTA). Her research focuses on increasing the reliability of critical software systems, by mathematically proving that the code behaves as expected and satisfies security and safety requirements. She contributed to the seL4 correctness proof and now focuses on concurrency reasoning for OS code. She leads the concurrency software verification research in Data61, and is deputy leader of the Trustworthy Systems group. She was recognised in 2011 by MIT’s Technology Review as one of the world’s top young innovators (TR35). She holds a PhD in Computer Science from the University of Paris-Sud, France.</p> </div> <h3>Links</h3> <ul> <li><a class="url u-url" href="https://galois.com/blog/2016/05/tech-talk-interrupts-in-os-code-lets-reason-about-them-yes-this-means-concurrency/">Website</a></li> </ul> </div>

You can edit, clone, or delete this event.

This item was added directly to Calagator
Monday, May 2, 2016 at 11:09am.

Galois tech talk: Interrupts in OS code: let’s reason about them. Yes, this means concurrency.

Wednesday, May 4, 2016 from 11am–noon

Galois Inc

421 Sw 6th Ave Ste 300

Portland, OR 97204, US (map)

Website

https://galois.com/blog/2016/05/tech-talk-interrupts-in-os-code-lets-reason-about-them-yes-this-means-concurrency/

Description

abstract:

Existing modeled and verified operating systems (OS’s) typically run on uniprocessor platforms and run with interrupts mostly disabled. This makes formal reasoning more tractable: execution is mostly sequential. The eChronos OS is a real-time OS used in tightly constrained devices, running on (uniprocessor) embedded micro-controllers. It is used in the DARPA-funded HACMS program, where it runs the flight control software of a high-assurance quadcopter. To provide low latency, the eChronos OS runs with interrupts enabled and provides a preemptive scheduler. In terms of verification, this means that concurrency reasoning is required, which significantly increases the complexity: application and OS instructions may be interleaved with interrupt handler instructions.

In our work we explicitly model the effect of interrupts and their handling by the hardware and OS. We provide a general formal model of the interleaving between OS code, application code and interrupt handlers. We then instantiate this model to formalise the scheduling behavior of the eChronos OS, and prove the main scheduler property: the running task is always the highest-priority runnable task.

bio:

June Andronick is a Senior Researcher at Data61|CSIRO (formerly NICTA). Her research focuses on increasing the reliability of critical software systems, by mathematically proving that the code behaves as expected and satisfies security and safety requirements. She contributed to the seL4 correctness proof and now focuses on concurrency reasoning for OS code. She leads the concurrency software verification research in Data61, and is deputy leader of the Trustworthy Systems group. She was recognised in 2011 by MIT’s Technology Review as one of the world’s top young innovators (TR35). She holds a PhD in Computer Science from the University of Paris-Sud, France.