Revise the rabbitmq controller to prevent unexpected downscale #211

euclidgame · 2023-08-13T20:00:45Z

The current version of RabbitMQ controller doesn't support scaling down; directly reducing the replicas of the stateful set can lead to quorum loss and even data loss. More details in this issue. Thus, we decide to disallow downscale for the stateful set in our implementation.

Using the validation rule can guarantee that updating the deployment won't decrease the replicas. But here is a corner case: a workaround for downscale operation is to delete the current deployment and create a new one with fewer replicas, which doesn't violate the validation rule. If the execution happens in this way, chances are that the stateful set created from the new cr may not have been deleted by the garbage collector when the controller tries to update the stateful set with the new cr which has a smaller replicas field. Thus, the controller implementation still needs to compare the old and new replicas before updating stateful set to make sure scaling down doesn't happen. This makes the proof a lot more difficult, because we have to show that the replicas of old stateful set is lower than that of the current cr, whose proof requires us to show that if a stateful set has owner reference pointing to some cr, its replicas is no larger.

Therefore, we decide to let the controller wait for the garbage collector to delete the old stateful set, which avoids the corner case, and does not introduce too much complexity to the proof since it's needless to compare the stateful set now. In this case, if the old stateful set doesn't have an owner reference pointing to the current cr, the reconcile will simply go to the error state and wait for the next round of reconcile.

To make the liveness proof work, I change the_object_in_reconcile_has_spec_as into the_object_in_reconcile_has_spec_and_uid_as so that the owner_references can also be derived from the desired custom resource. The left work is as follows:

Add an eventual safety property showing that spec /\ []desired_state_is(cr) |= true ~> (sts_key_exists => sts.owner_references.contains(cr.owner_ref())).
Add [](sts_key_exists => sts.owner_references.contains(cr.owner_ref())) to the assumption of the spec.
Add reasoning about the steps after create/update server config map and the stateful set part should be similar as zookeeper as long as 1 and 2 are done.

Signed-off-by: Wenjie Ma <rebekah1368@gmail.com>

.gitignore

Signed-off-by: Wenjie Ma <rebekah1368@gmail.com>

marshtompsxd · 2023-08-13T20:15:01Z

@euclidgame Thanks for the efforts. This is a super important PR. I will need to review it super carefully.

Can you revise the description as follows:
Rabbitmq controller does not support downscale, and why --> Start with we already use the validation rule to prevent downscale --> But there is still a corner case that downscale can happen, and explain the corner case --> thus, the controller implementation still needs to compare the old and new replicas before updating --> this makes the proof a lot more difficult, and why --> we decide to let the controller wait for the gc to delete the old statefulset, which avoids the corner case, and does not introduce too much complexity to the proof

tianyin · 2023-08-13T20:18:56Z

"super important PR" :)

src/controller_examples/rabbitmq_controller/exec/reconciler.rs

src/controller_examples/rabbitmq_controller/proof/common.rs

src/controller_examples/rabbitmq_controller/proof/helper_invariants.rs

src/controller_examples/rabbitmq_controller/proof/liveness.rs

marshtompsxd · 2023-08-13T20:58:38Z

src/controller_examples/rabbitmq_controller/proof/liveness.rs

@@ -744,17 +763,17 @@ proof fn lemma_from_pending_req_in_flight_at_some_step_to_pending_req_in_flight_
        // next_step != RabbitmqReconcileStep::Init,


You can remove it if not needed

marshtompsxd · 2023-08-13T20:59:11Z

src/controller_examples/rabbitmq_controller/proof/liveness.rs

@@ -912,21 +929,21 @@ proof fn lemma_from_resp_in_flight_at_some_step_to_pending_req_in_flight_at_next
        // We only know that rabbitmq_1.object_ref() == rabbitmq.object_ref() && rabbitmq_1.spec == rabbitmq.spec.
        forall |rabbitmq_1, resp_o|


similar comments as above

marshtompsxd · 2023-08-13T21:00:53Z

src/controller_examples/rabbitmq_controller/spec/rabbitmqcluster.rs

@@ -94,7 +105,8 @@ impl ResourceView for RabbitmqClusterView {
    }

    open spec fn transition_rule(new_obj: RabbitmqClusterView, old_obj: RabbitmqClusterView) -> bool {
-        true
+        new_obj.spec.replicas >= old_obj.spec.replicas
+        // true


You can remove the comment

src/kubernetes_cluster/proof/controller_runtime_safety.rs

marshtompsxd · 2023-08-13T21:17:31Z

src/kubernetes_cluster/proof/cluster.rs

@@ -125,6 +125,7 @@ pub open spec fn desired_state_is(cr: K) -> StatePred<Self>
        &&& s.resource_key_exists(cr.object_ref())
        &&& K::from_dynamic_object(s.resource_obj_of(cr.object_ref())).is_Ok()
        &&& K::from_dynamic_object(s.resource_obj_of(cr.object_ref())).get_Ok_0().spec() == cr.spec()
+        &&& K::from_dynamic_object(s.resource_obj_of(cr.object_ref())).get_Ok_0().metadata().uid == cr.metadata().uid


Actually, we don't have to change the desired_state_is predicate -- the fact that the cr always exists implies that its uid never changes. Could you leave a TODO here that later we will revert this predicate back?

I don't understand. Do you mean []cr_key_exists /\ next |= K::from_dynamic_object(s.resource_obj_of(cr.object_ref())).get_Ok_0().metadata().uid == cr.metadata().uid?

The cr here can be an arbitrary object, []cr_key_exists only shows that the uid of the cr object stored in etcd never changes, not the parameter cr here.

No, we don't want to say the uid is the same as cr.metadata().uid.
I was saying that we should treat uid similarly to the rest_id in the proof.
Basically, we no longer assume K::from_dynamic_object(s.resource_obj_of(cr.object_ref())).get_Ok_0().metadata().uid == cr.metadata().uid. Instead, you carry an uid as an argument (like the rest_id) in whatever lemma that needs the uid, with an extra precondition saying that []K::from_dynamic_object(s.resource_obj_of(cr.object_ref())).get_Ok_0().metadata().uid == uid.
Then, you can prove that whatever uid, if initially we have K::from_dynamic_object(s.resource_obj_of(cr.object_ref())).get_Ok_0().metadata().uid == uid, then it is always true that K::from_dynamic_object(s.resource_obj_of(cr.object_ref())).get_Ok_0().metadata().uid == uid (that is, uid remains unchanaged).
Finally, you can use leads_to_exists_intro to eliminate the uid. Just like https://github.com/vmware-research/verifiable-controllers/blob/main/src/controller_examples/zookeeper_controller/proof/liveness/liveness_property.rs#L208-L238

btw, I just realized that we should later revise pub open spec fn desired_state_is(cr: K) -> StatePred<Self> to pub open spec fn desired_state_is(key: ObjectRef, spec: K::Spec) -> StatePred<Self>. We only need the key and the spec here. I didn't do that because associated type was not there.

btw2, can we revise K::from_dynamic_object(s.resource_obj_of(cr.object_ref())).get_Ok_0().metadata().uid to s.resource_obj_of(cr.object_ref()).metadata.uid?

No, we don't want to say the uid is the same as cr.metadata().uid

This doesn't make sense to me. If the uid is not same as cr.metadata().uid, why should we care about that cr? I just think that we should only prove the liveness property about cr that always exists, so I think desired_state_is should say that that cr exists in ectd except the status thing you mentioned could be different.

why should we care about that cr?

I mean, we don't need to say that in the desired_state_is() (we want to minimize our assumption, if part of the predicate can be derived by the other parts), but I think it does no harm to keep it for now

nvm, let's also table this for now

Minimizing the assumption usually means getting a stronger property. But if strengthening the property is not useful, why should we minimize that?

I am confused: if the assumption desired_state_is() can be simpler (weaker) then why is it a bad thing? Or are you worried that weakening the assumption (for just one line) means many changes in the proof, so it is not worthwhile -- that I understand and agree.

marshtompsxd · 2023-08-13T21:23:23Z

I was looking for the reasoning for the statefulset and then I just realize that the proof is not done yet. Could you also summarize a list of the cosmetic changes made to the proof in the description (revise the last paragraph)?

Signed-off-by: Wenjie Ma <rebekah1368@gmail.com>

) This PR proves the liveness property of the rabbitmq controller. Different from the previous proof, this time both the liveness property and the state machine specification become more complex: the liveness property includes the stateful set object managed by the controller, and the state machine specification has been enriched a lot with validation rules, garbage collector, finalizer, and many other features. Besides, the implementation of the rabbitmq controller has changed: it waits for the garbage collector to recycle the stateful set of the old custom resource to avoid accidental downscale (see #211 ). All these factors make it even more challenging to prove liveness. ### Key challenges One of the key challenges during the proof is to identify and manage a large number of invariants. To give some concrete examples, here are two representative invariants: 1. If stateful set exists, then its owner reference must point to and only point to the current custom resource. 2. No delete request with the stateful set key will be sent to Kubernetes API. The first is used to show that finally stateful set created from old custom resources (if any) will be deleted, and this is done by the garbage collector. The second is to verify that if we get the desired stateful set, it will always exist. The proof of 2 requires 1 because we need it to show the garbage collector never tries to delete the stateful set (the gc actions is never enabled). Notably, though we call them "invariants", neither 1 nor 2 holds from the beginning of the execution (`init()`). That said, they are not the safety invariants that hold throughout the entire execution, but they start to hold at some point during the execution and continue to hold since then. Proving the liveness property requires a large number of such invariants, so how to prove and use them becomes a significant part of the proof burden. Note that the same problem exists even before this PR. ### Proof structure We notice that a common pattern in the liveness proof is that, to make the desired property eventually happens, the environment needs to first enter a state where there are no more perturbations that can interrupt the execution moving toward the desired property. For example, if we want the controller to make progress to the desired state, then we need to first prove that the controller stops crashing from a point. That said, the entire liveness proof, similar to the actual execution, is divided into phases. Starting from the initial phase (the initial state of the state machine), the system first enters a phase where perturbations (e.g., staleness, crashes, disturbing requests) no longer exist, then moves to the final phase where the desired state is achieved by the controller's correct execution. At each phase, we derive some invariants (the properties that hold from this point) which will be used to prove the properties of the next phase. Naturally, the invariants used in the proof can be grouped by the phase. They were referred to as `assumptions`, `invariants_since_rest_id`, `invariants_led_to_by_rest_id` (these variable names are indeed confusing, and we stop calling them in this way). In this proof, we divide the execution into different phase and invariants into several groups $I_1,I_2,\cdots,I_n$. More details in [this comment](#214 (comment)). In this structure, we often need to prove lemmas in the form of `spec |= true ~> []p`. If the property `p` talks about messages sent after a particular point, we often have to choose a `rest_id` and prove that eventually request messages before `req_id` are gone. This PR introduces a [lemma](https://github.com/vmware-research/verifiable-controllers/blob/f5783e1a014e7eedc76e38bfd82fa61de6d4cb98/src/kubernetes_cluster/proof/kubernetes_api_liveness.rs#L276C14-L276C75) in the `kubernetes_api_liveness` module to help reason about this kind of invariants, and the controller developers no longer need to directly reason about different `rest_id`s (And it's indeed better to avoid it). This improves both the reusability and the readability of the proof/lemmas. This PR does not try to finish proving all the invariants but focuses on ensuring that: 1. The invariants are grouped correctly into phases that follow the same logical order of the proof/execution. 2. The invariants should be provable with all antecedent invariants required. The phases of the invariants used in the liveness proof are: - 0: Invariants that hold throughout the entire execution (i.e., safety invariants). - 1: Crash and K8s busy are disabled, and the object that is in the schedule for reconciliation is updated. - 2: The object being reconciled is updated. - 3: Every creation and update request to the same object has the same effect. - 4: Objects only have their owner references pointing to the current cr, not the previously-deleted cr. - 5: No deletion requests are sent to the K8s API. --------- Signed-off-by: Wenjie Ma <rebekah1368@gmail.com>

euclidgame added 7 commits August 12, 2023 17:29

Reformat some code

2b0a0ac

Signed-off-by: Wenjie Ma <rebekah1368@gmail.com>

Rename safety -> helper_invariants

15bb574

Signed-off-by: Wenjie Ma <rebekah1368@gmail.com>

Set owner_references for rabbitmq controller

ef5ab84

Signed-off-by: Wenjie Ma <rebekah1368@gmail.com>

Change the rabbitmq controller implementation

3dc4924

Signed-off-by: Wenjie Ma <rebekah1368@gmail.com>

Prove controller_eventual_safety properties

282cef3

Signed-off-by: Wenjie Ma <rebekah1368@gmail.com>

Pop old changed

9975257

Signed-off-by: Wenjie Ma <rebekah1368@gmail.com>

Remove useless lemmas

1c25dc4

Signed-off-by: Wenjie Ma <rebekah1368@gmail.com>

euclidgame marked this pull request as ready for review August 13, 2023 20:02

euclidgame requested a review from marshtompsxd August 13, 2023 20:02