-
Notifications
You must be signed in to change notification settings - Fork 5
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Simplify liveness proof of zookeeper controller #166
Conversation
&&& s.reconcile_state_of(zk.object_ref()).pending_req_msg.is_Some() | ||
&&& s.message_in_flight(s.pending_req_of(zk.object_ref())) | ||
&&& is_create_stateful_set_request_msg(s.pending_req_of(zk.object_ref()), zk) | ||
pub open spec fn is_correct_pending_request_at_zookeeper_step( |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Like it!
lift_state(current_state_matches(zk)), | ||
always(lift_state(current_state_matches(zk))) | ||
); | ||
} | ||
|
||
proof fn lemma_from_pending_req_in_flight_at_some_step_to_next_step( |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This is nice!
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I am even thinking about whether we can further generalize this lemma (make it applicable to all controllers), but let's leave it for future PRs
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Could you document this lemma? Especially why we need these preconditions. The documentation will help us later a lot.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I am even thinking about whether we can further generalize this lemma
This is what we need to do later.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
And generalizing it seems not difficult but requires more handlings of "correct requests".
|
||
proof fn lemma_from_after_create_client_service_step_to_after_create_admin_server_service_step( | ||
spec: TempPred<ClusterState>, zk: ZookeeperClusterView, resp_msg: Message | ||
proof fn lemma_from_resp_in_flight_at_some_step_to_pending_req_at_next_step( |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Similarly, could you document this lemma?
&&& s_prime.message_in_flight(resp_msg) | ||
&&& resp_msg_matches_req_msg(resp_msg, req_msg) | ||
}); | ||
assert forall |s, s_prime| pre(s) && #[trigger] stronger_next(s, s_prime) implies pre(s_prime) || post(s_prime) by { |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Is this for proof stability?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Yes, it is.
step != ZookeeperReconcileStep::Error, step != ZookeeperReconcileStep::Done, | ||
next_step != ZookeeperReconcileStep::Init, | ||
forall |zk_1: ZookeeperClusterView, resp_o: Option<APIResponse>| | ||
#[trigger] reconcile_core(zk_1, resp_o, ZookeeperReconcileState{ reconcile_step: step }).0.reconcile_step == next_step |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I think this precondition wants to say no matter what, the next step is next_step
. I am trying to understand why we have to forall zk_1 here, instead of just talking about zk.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
We can't infer from the pre
state that the cr passed to reconcile_core
is exactly zk
. However, we may weaken the precondition for this lemma.
Signed-off-by: Wenjie Ma <[email protected]>
Signed-off-by: Wenjie Ma <[email protected]>
Signed-off-by: Wenjie Ma <[email protected]>
Signed-off-by: Wenjie Ma <[email protected]>
Signed-off-by: Wenjie Ma <[email protected]>
Signed-off-by: Wenjie Ma <[email protected]>
Signed-off-by: Wenjie Ma <[email protected]>
01c54de
to
3b3c165
Compare
Signed-off-by: Wenjie Ma <[email protected]>
Signed-off-by: Wenjie Ma <[email protected]>
// The proof is very straightforward: | ||
// - Right after the controller enters 'state', the pending request is added to in_flight. | ||
// - If the pending request is processed by kubernetes api, there will be a response in flight. | ||
// - If the response is processed by the controller, the controller will either enter a new state or a new pending request in flight. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
either enter a new state or a new pending request in flight
Or?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Yes. By this I mean the controller will not necessarily enter a new state; if it enters a state that is same as 'state', then a new pending request will be in flight, so in this case the invariant will not be violated.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I see what you mean. Maybe it is better to say "If the response is processed by the controller, the controller will either the next state (which could still be 'state' but the invariant still holds then)."
Signed-off-by: Wenjie Ma <[email protected]>
&&& s.reconcile_state_of(zk.object_ref()).pending_req_msg.is_Some() | ||
&&& is_create_config_map_request_msg(s.pending_req_of(zk.object_ref()), zk) | ||
&&& is_correct_pending_request_msg_at_zookeeper_step(step, s.pending_req_of(zk.object_ref()), zk, object) | ||
&&& s.message_in_flight(resp_msg) | ||
&&& resp_msg_matches_req_msg(resp_msg, s.pending_req_of(zk.object_ref())) | ||
} | ||
} |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I think the above spec functions can be made more generic and will be reused heavily. But to do so we might need to make the step
an associated type of Reconciler
and the spec functions need to take a closure for is_correct_pending_request_msg_at_zookeeper_step
. We can work on this later.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Absolutely.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
take a closure for
is_correct_pending_request_msg_at_zookeeper_step
Actually I have more thoughts about this... I will put it in the issue.
lift_state(current_state_matches(zk)), | ||
always(lift_state(current_state_matches(zk))) | ||
); | ||
} | ||
|
||
// This lemma ensures that zookeeper controller at some step with pending request in flight will finally enter its next step. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
To avoid ambiguity, you can say "This lemma ensures that zookeeper controller at step a with pending request in flight will finally enter step b." and use step a, step b below, instead of initial, final step. My first reaction when seeing initial step is actually ZookeeperReconcileStep::Init
// For the initial state and final state, they both require the reconcile_state to have a pending request which is the correct | ||
// request for that step (parameter 'step' for the initial step, parameter 'next_step' for the final state). | ||
// Note that in this lemma we add some constraints to the initial step: | ||
// 1. The next step of it when conducting reconcile_core is deterministic. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Instead of deterministic, I think what you mean is that there is only one possible next step (i.e., step b) for step a. The reconcile_core is still deterministic even with branches.
// request for that step (parameter 'step' for the initial step, parameter 'next_step' for the final state). | ||
// Note that in this lemma we add some constraints to the initial step: | ||
// 1. The next step of it when conducting reconcile_core is deterministic. | ||
// 2. When the controller enters this step, it must creates a request (which will be used to create the pending request message) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
"which will be used to create the pending request message" --> "which is piggybacked by the pending request message"
Typo: creates -> create
proof fn lemma_from_after_create_headless_service_step_to_after_create_client_service_step( | ||
spec: TempPred<ClusterState>, zk: ZookeeperClusterView, resp_msg: Message | ||
// This lemma ensures that zookeeper controller at some step with a response in flight that matches its pending request will finally enter its next step. | ||
// For the initial state and final state, they both require the reconcile_state to have a pending request which is the correct |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Similar comment as above. Try to avoid using initial and final here
// request for that step (parameter 'step' for the initial step, parameter 'result_step' for the final state). For the initial state | ||
// alone, there is a known response (the parameter resp_msg) in flight that matches the pending request. | ||
// Note that in this lemma we add some constraints to the initial step: | ||
// 1. The next step of it when conducting reconcile_core is deterministic. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Similar comment for "deterministic"
// alone, there is a known response (the parameter resp_msg) in flight that matches the pending request. | ||
// Note that in this lemma we add some constraints to the initial step: | ||
// 1. The next step of it when conducting reconcile_core is deterministic. | ||
// 2. When the controller enters this step, it must creates a request (which will be used to create the pending request message) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Similar comment
Signed-off-by: Wenjie Ma <[email protected]>
In this PR, I mainly do two things: