From Starvation Freedom to All-Path Reachability Problems in Constrained Rewriti...

on YouTube ↗25m

" summary

Extends LC term rewrite systems to reduce starvation freedom to an all-path reachability (APR) check by instrumenting states with a counter C with reset/increment rules and treating C > Cmax and certain terminating normal forms as error states; proves normal forms are finitely many constraint terms and implements the transformation and proof system. Tool verifies Peterson mutual exclusion as starvation-free in 7.39 seconds. Main limitations: Cmax must be chosen and APR failure only implies “maybe starvation.”

AI-written summary · about

" chapters (18)

1. 0:00Starvation freedom introduction
2. 1:52All-path reachability motivation
3. 2:35All-path reachability definition
4. 3:19Logically constrained rewrite systems
5. 4:03LCRS for async transitions
6. 6:15Constraint terms and APR validity
7. 7:19Runtime errors to APR problems
8. 8:44Race condition verification
9. 9:48Starvation freedom challenges
10. 10:53Counters for starvation detection
11. 12:00Modifying rules with counters
12. 13:52Error states with counter limits
13. 14:57Normal forms for termination
14. 17:31Starvation freedom in Peterson's
15. 19:16Starvation freedom proof
16. 20:42Implementation and results
17. 21:04Conclusion and future work
18. 22:37Q&A on disproof methods