Keywords

Lecture Notes

• Wk1
• L1
• Properties
• Limits and Boundaries
• L2
• LTL
• Critical section

• Wk2
• Transition Diagram
• Floyd Verification
• Owicki-Gries Method
• Assertion Network
• One Big Invariant

• Wk3
• L1
• Liveness desiderata
• Safety propoerties
• Szymanski’s Algorithm
• L2
• lock/mutex
• test and test and set

• Wk4
• L1
• Semaphore
• L2
• Monitor
• Disadvantage of Semaphore
• Persistent data structure

• Wk5
• Message Passing
• Synchronous transition diagram
• Adding Shared auxiliary variables (+Invariant)
• Levin & Gries-style proof
• AFR style proof

• Wk7
• L1
• Termination
• Well Founded order
• Floyd’s Wellfoundedness Method
• Owicki/Gries Deadlock-Freedom Condition
• L2
• Compositionality
• Partial Correctness
• Parallel composition rule

• Wk8
• L1
• Calculus of Communicating Systems
• Process algebra
• labelled transition system
• L2
• Neilsen-Mizuno Algorithm

• Wk9
• L1
• Commitment and Consensus
• L2
• Distributed System with an Environment Node
• Credit-recovery algorithms
• Chandy-Lamport