Skip to content

Commit

Permalink
Revise the rabbitmq controller to prevent unexpected downscale (#211)
Browse files Browse the repository at this point in the history 
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](rabbitmq/cluster-operator#223). Thus,
we decide to disallow downscale for the stateful set in our
implementation.

Using the [validation
rule](https://github.com/vmware-research/verifiable-controllers/blob/f5236647bf4fb26daa1359fde3c61a282a886735/src/controller_examples/rabbitmq_controller/spec/rabbitmqcluster.rs#L108)
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:
1. Add an eventual safety property showing that `spec /\
[]desired_state_is(cr) |= true ~> (sts_key_exists =>
sts.owner_references.contains(cr.owner_ref()))`.
2. Add `[](sts_key_exists =>
sts.owner_references.contains(cr.owner_ref()))` to the assumption of the
spec.
3. 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>
  • Loading branch information
@euclidgame
euclidgame committed Aug 13, 2023
1 parent d92059c commit 8503f64
Show file tree
Hide file tree
Showing 19 changed files with 1,468 additions and 1,101 deletions.
15 changes: 14 additions & 1 deletion src/controller_examples/rabbitmq_controller/exec/rabbitmqcluster.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,10 +2,12 @@
// SPDX-License-Identifier: MIT
use crate::kubernetes_api_objects::error::ParseDynamicObjectError;
use crate::kubernetes_api_objects::{
api_resource::*, common::*, dynamic::*, marshal::*, object_meta::*, resource::*,
api_resource::*, common::*, dynamic::*, marshal::*, object_meta::*, owner_reference::*,
resource::*,
};
use crate::pervasive_ext::string_view::*;
use crate::rabbitmq_controller::spec::rabbitmqcluster::*;
use deps_hack::kube::Resource;
use vstd::prelude::*;

verus! {
Expand Down Expand Up @@ -65,6 +67,17 @@ impl RabbitmqCluster {
ApiResource::from_kube(deps_hack::kube::api::ApiResource::erase::<deps_hack::RabbitmqCluster>(&()))
}

#[verifier(external_body)]
pub fn controller_owner_ref(&self) -> (owner_reference: OwnerReference)
ensures
owner_reference@ == self@.controller_owner_ref(),
{
OwnerReference::from_kube(
// We can safely unwrap here because the trait method implementation always returns a Some(...)
self.inner.controller_owner_ref(&()).unwrap()
)
}

// NOTE: This function assumes serde_json::to_string won't fail!
#[verifier(external_body)]
pub fn to_dynamic_object(self) -> (obj: DynamicObject)
Expand Down
132 changes: 112 additions & 20 deletions src/controller_examples/rabbitmq_controller/exec/reconciler.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@
use crate::external_api::exec::*;
use crate::kubernetes_api_objects::resource::ResourceWrapper;
use crate::kubernetes_api_objects::{
api_method::*, common::*, config_map::*, label_selector::*, object_meta::*,
api_method::*, common::*, config_map::*, label_selector::*, object_meta::*, owner_reference::*,
persistent_volume_claim::*, pod::*, pod_template_spec::*, resource::*,
resource_requirements::*, role::*, role_binding::*, secret::*, service::*, service_account::*,
stateful_set::*,
Expand Down Expand Up @@ -294,25 +294,29 @@ pub fn reconcile_core(rabbitmq: &RabbitmqCluster, resp_o: Option<Response<EmptyT
let get_sts_resp = resp_o.unwrap().into_k_response().into_get_response().res;
if get_sts_resp.is_ok() {
// update
let found_stateful_set = StatefulSet::from_dynamic_object(get_sts_resp.unwrap());
if found_stateful_set.is_ok(){
let mut new_stateful_set = found_stateful_set.unwrap();
// rabbitmq controller doesn't support scale down, so new replicas must be greater than or equal to old replicas
if new_stateful_set.spec().is_some()
&& new_stateful_set.spec().unwrap().replicas().is_some()
&& new_stateful_set.spec().unwrap().replicas().unwrap() <= rabbitmq.spec().replicas() {
new_stateful_set.set_spec(stateful_set.spec().unwrap());
let req_o = KubeAPIRequest::UpdateRequest(KubeUpdateRequest {
api_resource: StatefulSet::api_resource(),
name: stateful_set.metadata().name().unwrap(),
namespace: rabbitmq.namespace().unwrap(),
obj: new_stateful_set.to_dynamic_object(),
});
let state_prime = RabbitmqReconcileState {
reconcile_step: RabbitmqReconcileStep::AfterUpdateStatefulSet,
..state
};
return (state_prime, Some(Request::KRequest(req_o)));
let get_sts_result = StatefulSet::from_dynamic_object(get_sts_resp.unwrap());
if get_sts_result.is_ok(){
let mut found_stateful_set = get_sts_result.unwrap();
// We check the owner reference of the found stateful set here to ensure that it is not created from
// previously existing (and now deleted) cr. Otherwise, if the replicas of the current cr is smaller
// than the previous one, scaling down, which should be prohibited, will happen.
// If the found stateful set doesn't contain the controller owner reference of the current cr, we will
// just let the reconciler enter the error state and wait for the garbage collector to delete it. So
// after that, when a new round of reconcile starts, there is no stateful set in etcd, the reconciler
// will go to create a new one.
if found_stateful_set.metadata().owner_references_contains(rabbitmq.controller_owner_ref()) {
found_stateful_set.set_spec(stateful_set.spec().unwrap());
let req_o = KubeAPIRequest::UpdateRequest(KubeUpdateRequest {
api_resource: StatefulSet::api_resource(),
name: stateful_set.metadata().name().unwrap(),
namespace: rabbitmq.namespace().unwrap(),
obj: found_stateful_set.to_dynamic_object(),
});
let state_prime = RabbitmqReconcileState {
reconcile_step: RabbitmqReconcileStep::AfterUpdateStatefulSet,
..state
};
return (state_prime, Some(Request::KRequest(req_o)));
}
}
} else if get_sts_resp.unwrap_err().is_object_not_found() {
Expand Down Expand Up @@ -424,6 +428,17 @@ pub fn make_service(rabbitmq: &RabbitmqCluster, name:String, ports: Vec<ServiceP
let mut metadata = ObjectMeta::default();
metadata.set_name(name);
metadata.set_namespace(rabbitmq.namespace().unwrap());
metadata.set_owner_references({
let mut owner_references = Vec::new();
owner_references.push(rabbitmq.controller_owner_ref());
proof {
assert_seqs_equal!(
owner_references@.map_values(|owner_ref: OwnerReference| owner_ref@),
rabbitmq_spec::make_role(rabbitmq@).metadata.owner_references.get_Some_0()
);
}
owner_references
});
metadata.set_labels({
let mut labels = StringMap::empty();
labels.insert(new_strlit("app").to_string(), rabbitmq.name().unwrap());
Expand Down Expand Up @@ -502,6 +517,17 @@ pub fn make_secret(rabbitmq: &RabbitmqCluster, name:String , data: StringMap) ->
let mut metadata = ObjectMeta::default();
metadata.set_name(name);
metadata.set_namespace(rabbitmq.namespace().unwrap());
metadata.set_owner_references({
let mut owner_references = Vec::new();
owner_references.push(rabbitmq.controller_owner_ref());
proof {
assert_seqs_equal!(
owner_references@.map_values(|owner_ref: OwnerReference| owner_ref@),
rabbitmq_spec::make_role(rabbitmq@).metadata.owner_references.get_Some_0()
);
}
owner_references
});
metadata.set_labels({
let mut labels = StringMap::empty();
labels.insert(new_strlit("app").to_string(), rabbitmq.name().unwrap());
Expand All @@ -525,6 +551,17 @@ fn make_plugins_config_map(rabbitmq: &RabbitmqCluster) -> (config_map: ConfigMap
let mut metadata = ObjectMeta::default();
metadata.set_name(rabbitmq.name().unwrap().concat(new_strlit("-plugins-conf")));
metadata.set_namespace(rabbitmq.namespace().unwrap());
metadata.set_owner_references({
let mut owner_references = Vec::new();
owner_references.push(rabbitmq.controller_owner_ref());
proof {
assert_seqs_equal!(
owner_references@.map_values(|owner_ref: OwnerReference| owner_ref@),
rabbitmq_spec::make_role(rabbitmq@).metadata.owner_references.get_Some_0()
);
}
owner_references
});
metadata.set_labels({
let mut labels = StringMap::empty();
labels.insert(new_strlit("app").to_string(), rabbitmq.name().unwrap());
Expand All @@ -551,6 +588,17 @@ fn make_server_config_map(rabbitmq: &RabbitmqCluster) -> (config_map: ConfigMap)
let mut metadata = ObjectMeta::default();
metadata.set_name(rabbitmq.name().unwrap().concat(new_strlit("-server-conf")));
metadata.set_namespace(rabbitmq.namespace().unwrap());
metadata.set_owner_references({
let mut owner_references = Vec::new();
owner_references.push(rabbitmq.controller_owner_ref());
proof {
assert_seqs_equal!(
owner_references@.map_values(|owner_ref: OwnerReference| owner_ref@),
rabbitmq_spec::make_role(rabbitmq@).metadata.owner_references.get_Some_0()
);
}
owner_references
});
metadata.set_labels({
let mut labels = StringMap::empty();
labels.insert(new_strlit("app").to_string(), rabbitmq.name().unwrap());
Expand Down Expand Up @@ -611,6 +659,17 @@ fn make_service_account(rabbitmq: &RabbitmqCluster) -> (service_account: Service
let mut metadata = ObjectMeta::default();
metadata.set_name(rabbitmq.name().unwrap().concat(new_strlit("-server")));
metadata.set_namespace(rabbitmq.namespace().unwrap());
metadata.set_owner_references({
let mut owner_references = Vec::new();
owner_references.push(rabbitmq.controller_owner_ref());
proof {
assert_seqs_equal!(
owner_references@.map_values(|owner_ref: OwnerReference| owner_ref@),
rabbitmq_spec::make_role(rabbitmq@).metadata.owner_references.get_Some_0()
);
}
owner_references
});
metadata.set_labels({
let mut labels = StringMap::empty();
labels.insert(new_strlit("app").to_string(), rabbitmq.name().unwrap());
Expand All @@ -633,6 +692,17 @@ fn make_role(rabbitmq: &RabbitmqCluster) -> (role: Role)
let mut metadata = ObjectMeta::default();
metadata.set_name(rabbitmq.name().unwrap().concat(new_strlit("-peer-discovery")));
metadata.set_namespace(rabbitmq.namespace().unwrap());
metadata.set_owner_references({
let mut owner_references = Vec::new();
owner_references.push(rabbitmq.controller_owner_ref());
proof {
assert_seqs_equal!(
owner_references@.map_values(|owner_ref: OwnerReference| owner_ref@),
rabbitmq_spec::make_role(rabbitmq@).metadata.owner_references.get_Some_0()
);
}
owner_references
});
metadata.set_labels({
let mut labels = StringMap::empty();
labels.insert(new_strlit("app").to_string(), rabbitmq.name().unwrap());
Expand Down Expand Up @@ -739,6 +809,17 @@ fn make_role_binding(rabbitmq: &RabbitmqCluster) -> (role_binding: RoleBinding)
let mut metadata = ObjectMeta::default();
metadata.set_name(rabbitmq.name().unwrap().concat(new_strlit("-server")));
metadata.set_namespace(rabbitmq.namespace().unwrap());
metadata.set_owner_references({
let mut owner_references = Vec::new();
owner_references.push(rabbitmq.controller_owner_ref());
proof {
assert_seqs_equal!(
owner_references@.map_values(|owner_ref: OwnerReference| owner_ref@),
rabbitmq_spec::make_role(rabbitmq@).metadata.owner_references.get_Some_0()
);
}
owner_references
});
metadata.set_labels({
let mut labels = StringMap::empty();
labels.insert(new_strlit("app").to_string(), rabbitmq.name().unwrap());
Expand Down Expand Up @@ -785,6 +866,17 @@ fn make_stateful_set(rabbitmq: &RabbitmqCluster) -> (stateful_set: StatefulSet)
let mut metadata = ObjectMeta::default();
metadata.set_name(rabbitmq.name().unwrap().concat(new_strlit("-server")));
metadata.set_namespace(rabbitmq.namespace().unwrap());
metadata.set_owner_references({
let mut owner_references = Vec::new();
owner_references.push(rabbitmq.controller_owner_ref());
proof {
assert_seqs_equal!(
owner_references@.map_values(|owner_ref: OwnerReference| owner_ref@),
rabbitmq_spec::make_role(rabbitmq@).metadata.owner_references.get_Some_0()
);
}
owner_references
});
metadata.set_labels({
let mut labels = StringMap::empty();
labels.insert(new_strlit("app").to_string(), rabbitmq.name().unwrap());
Expand Down

0 comments on commit 8503f64

Please sign in to comment.