Formal Modeling of Software Caches
| Sponsors |
Ken
Mackenzie
kenmac@cc.gatech.edu
CoC 219
|
Pete Manolios
manolios@cc.gatech.edu
CRB 259A
|
|
|
Please contact one of the project sponsors before you start.
|
| Areas |
Formal Methods/Architecture |
Problem
The problem is to develop a formal model of a software cache using
the ACL2
theorem proving system.
A software cache is implemented by using dynamic binary
rewriting to implement cache/MMU functionality for a computer system
that does not include this functionality in hardware. Systems that
benefit from software caches include soft
architectures.
In order to guarantee that the software cache behaves as intended, we
will use formal techniques. This includes the following
steps.
- Modeling the problem formally. This means using a system
with an unambiguous semantics and a proof theory. The system we will use is ACL2. ACL2
consists of a programming language based on applicative Common Lisp,
a logic, and a theorem prover. You can think of the model as a
simulator and in fact, you will be able to run it.
- Defining what it means for the software cache to be
correct. Correctness will be expressed as a relationship
between the system without the software cache and the system with the
cache.
- Proving that the software cache satisfies its specification.
You are not responsible for this part, but if you are interested in
exploring the issues, let us know.
Background
To undertake this project, it would help if one has a basic understanding of
hardware caching and has some experience with Lisp. Here are some
relevant pointers.
Deliverables
- Simulation model, including a statement of correctness.
- Short report documenting the work.
Evaluation
Evaluation is based on the quality of the model and report.