A Note on Symbolic Reachability Analysis Modulo Integer Constraints for the CASH Algorithm
This page reports on the application of rewriting modulo SMT by Kyungmin Bae and Camilo Rocha, at the University of Illinois at Urbana-Champaign, to specify and analyze symbolically the CASH scheduling algorithm, a sophisticated state-of-the-art scheduling algorithm with advanced capacity sharing features for reusing unused execution budgets. The CASH algorithm had been developed by Caccamo, Buttazzo, and Sha at the University of Illinois at Urbana-Champaign. Because the number of elements in the queue of unused resources can grow beyond any bound, the CASH algorithm poses challenges to its formal specification and analysis. This scheduling algorithm had been subject of ground formal analysis in Real-time Maude by Ölveczky and Caccamo (more information available here).
The reason for the analysis was that Bae and Rocha wanted to experiment with the effectiveness of rewriting modulo SMT for finding minimal counter-examples, a laborious task when using the ground specification of the CASH algorithm in Real-time Maude. A symbolic state in the symbolic CASH specification is a pair (φ,conf) where φ is a linear integer constraint and conf is an configuration (or multiset) of objects that can mention the variables in the constraint φ. Symbolic states have initial model semantics, i.e., a state (φ,conf) denotes the set of ground states θ(conf) such that θ(φ) is valid in the standard model of the theory of integer numbers. Then, the rewriting modulo SMT relation is a binary relation on symbolic states that have initial model semantics.
It is particularly interesting that by using the techniques for rewriting modulo SMT developed by Rocha in his Ph.D. thesis and an extension of Maude with CVC3 for solving the linear integer constraints, one could use directly Maude's search and LTL model checking commands to perform symbolic reachability analysis for the CASH algorithm. In the experiment we could detect, by using Maude's search command, a minimal symbolic counter-example for a symbolic initial configuration comprising infinitely many ground states in less than 2 seconds after only visiting 234 symbolic states.
|The Executable Symbolic Specification of the CASH Algorithm|