Lars Birkedal, Aleš Bizjak
Iris is a framework that can be used for reasoning about safety of concurrent programs, as the logic in logical relations, to reason about type-systems, data-abstraction etc. In case of questions, please contact us in our chat room.
Below we provides notes from a lecture introducing to Iris. The lecture notes have been used in an M.Sc. level course at Aarhus University. See the iris-project.org page for an overview of research that uses Iris one way or another.
| Week | Day | Lecture | Literature | Slides | Hand-in Exercises |
|---|---|---|---|---|---|
| 1 | Day 1 | Intro + Operational Semantics | ILN Sec. 1+2 | lecture1 | |
| Day 2 | Basic Logic of Resources | ILN Sec. 3 | lecture2 | ILN Ex. 3.2 | |
| 2 | Day 1 | Basic Separation Logic: Hoare Triples | ILN Sec. 4.0 | lecture3 | |
| Day 2 | Basic Separation Logic: Proving Pointer Programs | ILN Sec. 4.1 | lecture4 | ILN Ex. 4.1, 4.2, 4.5, 4.11, 4.21 | |
| 3 | Day 1 | Basic Separation Logic: Abstract Data Types | ILN Sec. 4.2 | lecture5 | |
| Day 2 | Case Study: foldr | ILN Sec. 4.3 | lecture6 | ILN Ex. 4.29, 4.34 | |
| 4 | Day 1 | Later Modality | ILN Sec. 5 | lecture7 | |
| Day 2 | Always Modality | ILN Sec. 6 | lecture8 | ILN Ex. 5.3, 6.2 item (1) (2) and (4) | |
| 5 | Day 1 | Concurrency: par + invariants | ILN Sec. 7.1 + 7.2 | lecture9 | |
| Day 2 | Concurrency: ghost state | ILN Sec. 7.4 + 7.5 | lecture10 | ILN Ex. 7.6, 7.24 item (3), 7.29, 7.32 (the first triple) | |
| 6 | Day 1 | Concurrency: Case Study: spin lock + concurrent bag | ILN Sec. 7.6 | lecture11 | |
| Day 2 | Concurrency: Case Study: counter modules | ILN Sec. 7.7 | lecture12 | ILN Ex. 7.37, 7.42. | |
| 7 | Day 1 | Weakest preconditions and fancy update modality | ILN Sec. 8.1 + 8.2 | lecture13 | |
| Day 2 | Concurrency: Case Study: concurrent stack with helping | ILN Sec. 10 | lecture14 | ILN Ex. 7.43 (the one for incr), 7.47, 7.49 (the two specs for read). |