ARC model specified in spinroot/promela

Hello hackers,

I'm writing to introduce a project I've been working on off-and-on for a
while now - verifying parts of kernel code using a formal specifier[1]

Please find attached a patch to try out a formal verification run of the
Adaptive Replacement Cache by Megido et.al. [2]

You can try it out by installing spin from your favourite package
manager, and then running "make" in the current directory - it just
needs the usual C toolchain, afaik.

I'm hoping that someone can help me complete the current run, as I don't
have the computing resources required to run the full model (about 16GB
RAM). Meanwhile I'll keep finding ways to reduce the statespace
required.

The idea here is that once verified, the model can be written up as C
code, and then re-exracted using the modex [3] tool

I have some unpublished work that demonstrates this using the md(4)
NetBSD driver, but I want to be able to do a clean-room implementation
first, in order to get a better sense of a developer methodology I'm
going to call "DDD" or "D3" (Design Driven Development).

Bricks and boquets welcome. (Please Cc: me, as I am not subscribed to
the ML)

[1] https://spinroot.com/spin/whatispin.html
[2] https://www.usenix.org/legacy/events/fast03/tech/full_papers/megiddo/megiddo.pdf Fig. 4
[3] http://spinroot.com/modex/MANUAL.html

Best,
-- 
~cherry