MetaData storage specification

[andrershov]

This PR adds metadata storage specification to prove that the way our storage layer underlying Zen2 implementation works correctly.
This specification does no model multipath, only a single data path is modeled.

[DaveCTurner]

Looks good!

I suggest modelling the existence of files using the domain of metadata and manifest rather than using -1 sentinels: DaveCTurner@937a7b8

This would also means you could remove steps and limit the model size with a constraint like newMeta < 4. (Also, this should really be a state constraint not an action constraint).

(edit: I suggested newMeta < 4 /\ newManifest < 4 but in fact the newMeta constraint is enough)

[andrershov]

@DaveCTurner thanks for your review! Modelling with domains looks much nicer. However, I'm not sure if we can avoid steps constraint. I've tried newMeta < 4 /\ newManifest < 4 and seems that the model is hanging.
In fact, the model can take the infinite number of execution steps without incrementing newMeta using the following execution path writeMeta -> writeMetaFail -> deleteMeta -> writeMeta -> writeMetaFail -> deleteMeta...

[DaveCTurner]

In fact, the model can take the infinite number of execution steps without incrementing newMeta using the following execution path...

This is true, but if you remove steps then the state space becomes finite. An infinite path through a finite state space can be checked in finite time, because the model checker deduplicates its states.

[andrershov]

@DaveCTurner thanks for your explanation, the reason why the model was running indefinitely is that I forgot to remove steps variable from the model and the number of states was infinite. Fixed by this commit d1346d7 .
I'm not sure if we shall commit the buggy version or correct implemented version to the repository. I think it's better to commit the correct implemented version.

[andrershov]

@DaveCTurner I've made a change to the specification by splitting deleteNew and deleteOld into separately deleting manifest and metadata files, which makes clearer in my opinion. Ready for the next pass.

[DaveCTurner]

LGTM