Prove safety property on scaling-down for Rabbitmq controller #220
Conversation
euclidgame
force-pushed
the
rabbitmq_safety
branch
from
2b50ee8
to
75f5198
Compare
…controller Signed-off-by: Wenjie Ma <[email protected]>
| @@ -1112,4 +1096,124 @@ pub proof fn lemma_true_leads_to_always_no_delete_sts_req_is_in_flight(spec: Tem | |||
| ); | |||
| } | |||
|
|
|||
| /// This spec tells that when the reconciler is at AfterGetStatefulSet, and there is a matched response, the reponse must be | |||
There was a problem hiding this comment.
We can probably have a lemma saying that for any get request, the matched get response has the same object key in its content, which applies to all controllers.
There was a problem hiding this comment.
The thing is we still need a lemma to say that at get stateful set step the pending request is xxx. So I decided to wrap the two. But it does no harm to write the lemma you mentioned.
euclidgame
force-pushed
the
rabbitmq_safety
branch
from
3363833
to
f9f3d41
Compare
|
@euclidgame, you must sign every commit in this pull request acknowledging our Developer Certificate of Origin before your changes are merged. This can be done by adding
|
Add from_dynamic_object_result_determined_by_unmarshal. Use spec as parameters for some lemmas. --------- Signed-off-by: Wenjie Ma <[email protected]>
Prove some of the helper invariants. Then assume the left hold, prove top level safety property. --------- Signed-off-by: Wenjie Ma <[email protected]>
Signed-off-by: Wenjie Ma <[email protected]>
Add generics to the Message Type. --------- Signed-off-by: Wenjie Ma <[email protected]>
Compact some similar lemmas. Try to delete some useless functions. Move some lemmas to common module (i.e, kubernetes_cluster::proof, not specific to one controller). Refactor the file structure to make it more reasonable. Reword some comments and naming. Try to make the verification more stable. Rename lower_rv => smaller_rv. --------- Signed-off-by: Wenjie Ma <[email protected]>
Signed-off-by: Wenjie Ma <[email protected]>
euclidgame
force-pushed
the
rabbitmq_safety
branch
from
f9f3d41
to
fe5bfa3
Compare
marshtompsxd
changed the title
marshtompsxd
changed the title
| ); | ||
| } | ||
|
|
||
| pub open spec fn ok_get_response_msg() -> FnSpec(MsgType<E>) -> bool { |
There was a problem hiding this comment.
Maybe is_ok_get_response_msg?
| && msg.content.get_get_response().res.is_Ok() | ||
| } | ||
|
|
||
| pub open spec fn ok_get_response_msg_with_key(key: ObjectRef) -> FnSpec(MsgType<E>) -> bool { |
There was a problem hiding this comment.
Maybe is_ok_get_response_msg_and_matches_key
| msg.src.is_KubernetesAPI() | ||
| && msg.content.is_get_response() | ||
| && msg.content.get_get_response().res.is_Ok() | ||
| && msg.content.get_get_response().res.get_Ok_0().object_ref() == key |
There was a problem hiding this comment.
I think we can later rename object_ref() to key() or sth, to avoid confusion with another reference (owner reference)
There was a problem hiding this comment.
Actually what is the source of object_ref?
There was a problem hiding this comment.
It's a datatype defined in kube-rs library, but we don't have to follow the name.
There was a problem hiding this comment.
I don't think this will cause confusion. Owner reference means reference of the owner, and I never omit "owner" when referring to it.
There was a problem hiding this comment.
@euclidgame I see you were documenting the invariants in #223 . Do you want to copy some documents here?
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]>
Prove the property that stateful set never scales down in rabbitmq controller. Details can be found in #223 . To supplement is, the concrete invariants in the code are as follows:
stateful_set_not_scaled_downobject_in_sts_update_request_has_smaller_rv_than_etcdreplicas_of_stateful_set_update_request_msg_is_no_smaller_than_etcdreplicas_of_etcd_stateful_set_satisfies_orderobject_in_ok_get_response_has_smaller_rv_than_etcdresponse_at_after_get_stateful_set_step_is_sts_get_responseobject_in_ok_get_resp_is_same_as_etcd_with_same_rvreplicas_of_stateful_set_create_or_update_request_msg_satisfies_orderetcd_and_scheduled_and_triggering_cr_in_correct_orderobject_in_every_create_or_update_request_msg_only_has_valid_owner_referencesevery_owner_ref_of_every_object_in_etcd_has_different_uid_from_uid_counterEach corresponds to a spec function.