I have just managed to write a refinement of my version of a TwoPhase spec to TCommit as is described in the video courses.
If you want to have a look at it, you need to download three repositories :
1 . Linear termporal definitions in Agda.
2. Temporal logic of Actions in Agda.
3. TLA examples
I define the notion of refinement locally , per action. If the conditions of the action hold for a specific behavior at a specific time, the conditions of the refined action must hold too.
The TwoPhase spec cannot refine the TCommit spec per action because the Decide action
contains a global condition that we do not want to have at the TwoPhase spec.
We need to prove global invariants for the TwoPhase Commit to be able to prove refinement.
One such invariant is this one : If the leader has sent a "commit" msg to the Resource Managers, then all RM are either prepared or committed.
The proof is done by induction, and it needs to be done for each action of the spec. The proof of the global Invariant is done locally. at each refinement of an action.
The reason I did this is because I wanted to be able to iteratively introduce global invariants, actions and variables while I was proving the refinement of the spec. In fact, I wanted both the refinement restrictions and the global invariants to guide the introduction of new actions.
So I couldn't prove the global invariants after I had provided the actions of the spec, because then, they would simply act as a proof obligation, and not as a guide.
In my opinion , this has proven to be a success. Proof obligations and types can guide refinement. The iterative method of introducing new actions, variables and global invariants has though some problems. Due to the iterative process, the global invariants that are selected are not good. They are not reusable in other parts of the refinement.
In the TwoPhase spec , these are the gi :
```
| gcondv : ∀{RM} → GCondV (TPVars RM) (suc (suc (suc (suc (suc (suc zero)))))) |
| gcondv {RM} (rmState , lmsgs , tprepared , rmsgs , rm) |
| = (doCommit ∈ˡ lmsgs → canCommit rmState) |
| ∷ (doAbort ∈ˡ lmsgs → notCommitted rmState) |
| ∷ (doCommit ∈ˡ lmsgs → doAbort ∉ˡ lmsgs) |
| ∷ ((e : Fin RM) → lmsgs ≡ ⊥ᶠ → e ∈ᶠ tprepared → (canCommit′ rmState) e) |
| ∷ (lmsgs ≡ ⊥ᶠ → notCommitted rmState) |
| ∷ (lmsgs ≡ ⊥ᶠ → (e : Fin RM) → e ∈ᶠ rmsgs → (canCommit′ rmState) e) |
∷ []
```
The 4th and 6th invariant could have been like this :
4 . If there is a commit msg , then the set of prepared RM(tprepared) contains all the RMs.
6. If a RM is in the set tprepared , then it has sent a msg that it is prepared.
These different global invariants would't help us prove things iteratively, because they require the knowledge of the remaining GI and the remaining variables.
I think that the best strategy when the spec has global invariants, is to first understand the spec globally, write down all the global invariants and the variables that are required by the GI and then use them to guide you when you introduce new actions and variables.
It seems to me that knowing the GI before hand, will also require that you know some of the actions before hand.
What do you think? For me , it is important that refinement is guided with the use of types. I think that I have succeeded. Here is an important question I have : Assuming that we have worked on paper a specific spec, and we think that we know which invariants are needed, what is the fastest way to put those thoughts to the test? The more we wait, the bigger the cost when our reasoning is wrong.
|