Proof of the safety property that stateful set never scales down in rabbitmq

[euclidgame]

This issue serves as an explanation of #220 .

Context and Problem

Implementation

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 also decide to disallow downscale for the stateful set in our implementation. We first change the rabbitmq controller implementation to wait for the garbage collector to delete the old stateful set. This, on top of the validation rule can guarantee that updating the deployment won't decrease the replicas. More details in PR #211 .

Proof

After implementing rabbitmq controller in the aforementioned way, we want to formally prove that in all possible executions in our current state machine, stateful set actually never gets updated with a lower replicas.

Formalism

To prove the safety property about stateful set, we need to first specify what the property is.

Previously, we planned to use Message to describe the possible update/deletion/creation actions, and also specify the relevant properties. However, it is better not to include Message in the description the high-level safety property because Message is just a tool and a detail of the system. For update action, one way to circumvent using Message is to talk about the previous and current state: an object being updated means that it exists in both states but changes in current state. As for the property in this issue, we can specify it in this way:

spec fn stateful_set_not_scaled_down(rabbitmq: RabbitmqClusterView) -> ActionPred<RMQCluster> {
    |s: RMQCluster, s_prime: RMQCluster| {
        let sts_key = make_stateful_set_key(rabbitmq.object_ref());
        s.resource_key_exists(sts_key)
        && s_prime.resource_key_exists(sts_key)
        ==> replicas_of_stateful_set(s_prime.resource_obj_of(sts_key)) >= replicas_of_stateful_set(s.resource_obj_of(sts_key))
    }
}

The property will be forall |rabbitmq| always(stateful_set_not_scaled_down(rabbitmq)). We don't have to require that the stateful set objects are different in the two states, because if it stays unchanged, the property won't be harmed.

Proof

Overview

The proof of this property mainly consists of reasoning about the replicas of etcd objects, create and update request messages, scheduled custom resource object and custom resource objects in reconcile. I will discuss the invariants we prove, what they are and what they are used for in the rest of this PR. I will number all of those invariants for better understanding.

Replicas Order

First, we define a replicas order for stateful set object:

spec fn replicas_satisfies_order(obj: DynamicObjectView, rabbitmq: RabbitmqClusterView) -> StatePred<RMQCluster>
    recommends
        obj.kind.is_StatefulSetKind(),
{
    |s: RMQCluster| {
        let key = rabbitmq.object_ref();
        let sts_replicas = replicas_of_stateful_set(obj);
        &&& s.resource_key_exists(key)
            && obj.metadata.owner_references_only_contains(RabbitmqClusterView::from_dynamic_object(s.resource_obj_of(key)).get_Ok_0().controller_owner_ref())
            ==> sts_replicas <= replicas_of_rabbitmq(s.resource_obj_of(key))
        &&& s.reconcile_scheduled_for(key)
            && obj.metadata.owner_references_only_contains(s.reconcile_scheduled_obj_of(key).controller_owner_ref())
            ==> sts_replicas <= s.reconcile_scheduled_obj_of(key).spec.replicas
        &&& s.reconcile_state_contains(key)
            && obj.metadata.owner_references_only_contains(s.triggering_cr_of(key).controller_owner_ref())
            ==> sts_replicas <= s.triggering_cr_of(key).spec.replicas
    }
}

obj can be the etcd statful set object, the object in create/update stateful set object. We define this order because, the replicas in the update request is derived from the triggering cr; so, in order to show the updated replicas is no smaller than the original one, we need to show that the original one (the one stored in etcd)'s replicas is no larger than that of triggering cr. obj.metadata.owner_references_only_contains(s.triggering_cr_of(key).controller_owner_ref()) here is to ensure that the cr is still the one that creates the stateful set object. The left two comparison is to assist the last one because when the state moves to the next state, the triggering_cr may be assigned (inserted or updated).

Invariants

All Invariants

• Invariant 1: Stateful set will not scale down.
• Invariant 2: Object in every valid stateful set update request message should specify its resource version and its resource version is smaller than the state resource version counter.
• Invariant 3: Object in every valid stateful set update request message (i.e, it should have the same resource version as the etcd stateful set), has no smaller replicas than the etcd object.
• Invariant 4: If the stateful set exists in etcd, its replicas should satisfy the replicas order.
• Invariant 5: Object in every ok stateful set get response message should specify its resource version and its resource version is smaller than the state resource version counter.
• Invariant 6: The response received at AfterGetStatefulSet step, if ok, should have its object with stateful set key as its reference.
• Invariant 7: Object in every ok get response, if with same resource version, is the same as the one in etcd.
• Invariant 8: Object in every valid create or update stateful set request message should satisfy the replicas order.
• Invariant 9: For a given cr_key, replicas_of(s.resource_obj_of(cr_key)) <= replicas_of(s.reconcile_scheduled_obj_of(cr_key)) <= replicas_of(s.triggering_cr_of(cr_key)). We prove the order of each two of them, if both cr exist and have the same uid.
• Invariant 10: Object in every valid create or update stateful set request message should have valid owner references, i.e. each of its owner references points to an ever existing object.
• Invariant 11: Every object in etcd should have valid owner references, i.e. each of its owner references points to an ever existing object.

These invariants also use some previously proved invariants, which I omit in this issue.

Dependencies

The following graph demonstrates the dependencies of all the aforementioned invariants.

graph TD;
1-->2;
1-->3;
3-->2;
2-->5;
2-->6;
3-->4;
3-->7;
3-->6;
4-->8;
4-->11;
8-->9;
8-->10;
11-->10;

Loading

Generality

When proving properties (invariants in this issue), we should consider whether they are specific to the controller, or can directly apply to any controller, or can apply to other controllers if we add some restrictions to the controller.

[euclidgame]

Invariant 1

This invariant is exactly the high-level property. The proof of this invariant is where we talk about update Message. It requires another two invariants (2 and 3) to hold all the time.

Invariant 2 is to show that every stateful set update request must specify the resource version because stateful set is allowed to update unconditionally. If resource version can be none, we can't rule out invalid update request through resource version. Invariant 3 is quite obvious.

[euclidgame]

Invariant 2 and 3

Since update request message for stateful set (at least in rabbitmq controller) is derived from the response of get request (and the response should be an ok one), we rely on some properties of matched get response message.

For invariant 2, we need invariant 5 and 6. The necessity of invariant 5 is self-explanatory. But invariant 5 alone is not enough, how can we know that when updating the stateful set, the response is a ok get response? We only know it's okay since it enters the update branch. We need invariant 6 to claim it's a get response; actually, an invariant that the request at AfterGetStatefulSet step is get request is already enough.

For invariant 3, we need invariants 2, 4, 6, 7. Invariant 3 mainly talks about the replicas of the object inside the update stateful set request. We know that replicas is part of spec, and the spec is assigned from the cr in reconcile.

• Without invariant 4, we can't know that the replicas of the stateful set object that is created by current cr, is no larger that that of the triggering cr, also that of the stateful set inside the update request messgae.
• Note that in invariant 4, the order between the replicas of stateful set in etcd and the cr in reconcile requires that the stateful set's owner reference points to the triggering cr. Without invariant 7, we can't know that the stateful set in etcd that has the same rv as the object in get response is that same as the object in get response (thus, they also have the same owner reference). The rv of update message is the same as get response message, and that's why we have requirements about the resource_version of update request message.
• From the last bullet, we can see that we need invariant 2 and 6 to show that the response if an ok get response of stateful set.

[euclidgame]

Invariant 4

To do the induction for this invariant, we mainly proves how the invariant holds if the stateful set in etcd is not changed (neither created not updated) from the previous state. If the state changes, we rely on the property of create/update request message which is proved in another lemma.

If the stateful set in ectd is the same as previous state (they don't have it or have the same one), we consider the cr key in etcd, scheduled_reconciles and ongoing_reconciles. If cr key doesn't exist in previous state, this means that it must not be the one the stateful set object's owner reference points to (thanks to invariant 11). If the previous state doesn't schedule reconcile for cr key, it means cr key exists in etcd in previous state, and the reconciled object is the same as that cr. Similarly, we can prove the order for triggering cr.

[euclidgame]

Invariant 5 and 7

The proof of these invariants is straightforward.

[euclidgame]

Invariant 6

We first prove that the pending request at this step is get stateful set request, which means its key is the key of stateful set. Then we prove a generic lemma for all ok get response message, that, if it matches one request pending at the controller side, the key of the object inside it should be the same as the key of that pending request.

[euclidgame]

Invariant 8

This invariant says that object in every valid create or update stateful set request message should satisfy the replicas order. As mentioned before, the replicas of that object is the same as that of the cr in reconcile. So we need:

• Invariant 9: for informing the verifier of the replicas order among the three custom resource objects.
• Invariant 10: for contradicting the cases when cr gets updated in etcd, because in that case, the cr is no longer pointed by the object's owner references.

[euclidgame]

Invariant 9

We prove three invariants (each two cr of the three) and integrate. them into one. We can't simply prove two orders, because the scheduled cr may not exist so it can't serve as an intermediary.

I move this invariant to a common module and require the transition_rule to be reflexive and transitive. By reflexive, I only require the spec of two objects to be the same. (Later if we support status, we can make some modifications).

Invariant 10 and 11

Due to our modifications to the implementation, it's straightforward to prove invariant 10. Then we can rely on it to prove invariant 11. Since etcd itself won't set the owner references of the object, we are already there.