From a6a41a4429b96b0986c607b7121cf3140fc244d7 Mon Sep 17 00:00:00 2001 From: Xudong Sun Date: Wed, 20 Sep 2023 16:06:57 -0500 Subject: [PATCH 1/3] Remove kind from UpdateRequest Signed-off-by: Xudong Sun --- .../rabbitmq_controller/spec/reconciler.rs | 16 +++++----- .../zookeeper_controller/spec/reconciler.rs | 18 +++++++---- src/kubernetes_api_objects/api_method.rs | 20 +++++++++---- .../proof/builtin_controllers.rs | 2 +- .../spec/client/state_machine.rs | 2 +- .../spec/kubernetes_api/state_machine.rs | 30 ++++++++----------- src/kubernetes_cluster/spec/message.rs | 7 +++-- 7 files changed, 54 insertions(+), 41 deletions(-) diff --git a/src/controller_examples/rabbitmq_controller/spec/reconciler.rs b/src/controller_examples/rabbitmq_controller/spec/reconciler.rs index 144dd9973..fba954538 100644 --- a/src/controller_examples/rabbitmq_controller/spec/reconciler.rs +++ b/src/controller_examples/rabbitmq_controller/spec/reconciler.rs @@ -163,7 +163,8 @@ pub open spec fn reconcile_core( { let found_config_map = ConfigMapView::unmarshal(get_config_resp.get_Ok_0()).get_Ok_0(); let req_o = APIRequest::UpdateRequest(UpdateRequest { - key: make_server_config_map_key(rabbitmq.object_ref()), + namespace: rabbitmq.metadata.namespace.get_Some_0(), + name: make_server_config_map_name(rabbitmq.metadata.name.get_Some_0()), obj: update_server_config_map(rabbitmq, found_config_map).marshal(), }); let state_prime = RabbitmqReconcileState { @@ -295,10 +296,11 @@ pub open spec fn reconcile_core( // update if StatefulSetView::unmarshal(get_sts_resp.get_Ok_0()).is_Ok() { let found_stateful_set = StatefulSetView::unmarshal(get_sts_resp.get_Ok_0()).get_Ok_0(); - if found_stateful_set.metadata.owner_references_only_contains(rabbitmq.controller_owner_ref()) + if found_stateful_set.metadata.owner_references_only_contains(rabbitmq.controller_owner_ref()) && found_stateful_set.spec.is_Some() { let req_o = APIRequest::UpdateRequest(UpdateRequest { - key: make_stateful_set_key(rabbitmq.object_ref()), + namespace: rabbitmq.metadata.namespace.get_Some_0(), + name: make_stateful_set_name(rabbitmq.metadata.name.get_Some_0()), obj: update_stateful_set( rabbitmq, found_stateful_set, state.latest_config_map_rv_opt.get_Some_0() @@ -565,16 +567,16 @@ pub open spec fn make_server_config_map(rabbitmq: RabbitmqClusterView) -> Config new_strlit("total_memory_available_override_value = 1717986919\n")@ } }); - if rabbitmq.spec.rabbitmq_config.is_Some() && rabbitmq.spec.rabbitmq_config.get_Some_0().advanced_config.is_Some() + if rabbitmq.spec.rabbitmq_config.is_Some() && rabbitmq.spec.rabbitmq_config.get_Some_0().advanced_config.is_Some() && rabbitmq.spec.rabbitmq_config.get_Some_0().advanced_config.get_Some_0() != new_strlit("")@ - && rabbitmq.spec.rabbitmq_config.get_Some_0().env_config.is_Some() + && rabbitmq.spec.rabbitmq_config.get_Some_0().env_config.is_Some() && rabbitmq.spec.rabbitmq_config.get_Some_0().env_config.get_Some_0() != new_strlit("")@ { data.insert(new_strlit("advanced.config")@, rabbitmq.spec.rabbitmq_config.get_Some_0().advanced_config.get_Some_0()) .insert(new_strlit("rabbitmq-env.conf")@, rabbitmq.spec.rabbitmq_config.get_Some_0().env_config.get_Some_0()) - } else if rabbitmq.spec.rabbitmq_config.is_Some() && rabbitmq.spec.rabbitmq_config.get_Some_0().advanced_config.is_Some() + } else if rabbitmq.spec.rabbitmq_config.is_Some() && rabbitmq.spec.rabbitmq_config.get_Some_0().advanced_config.is_Some() && rabbitmq.spec.rabbitmq_config.get_Some_0().advanced_config.get_Some_0() != new_strlit("")@ { data.insert(new_strlit("advanced.config")@, rabbitmq.spec.rabbitmq_config.get_Some_0().advanced_config.get_Some_0()) - } else if rabbitmq.spec.rabbitmq_config.is_Some() && rabbitmq.spec.rabbitmq_config.get_Some_0().env_config.is_Some() + } else if rabbitmq.spec.rabbitmq_config.is_Some() && rabbitmq.spec.rabbitmq_config.get_Some_0().env_config.is_Some() && rabbitmq.spec.rabbitmq_config.get_Some_0().env_config.get_Some_0() != new_strlit("")@ { data.insert(new_strlit("rabbitmq-env.conf")@, rabbitmq.spec.rabbitmq_config.get_Some_0().env_config.get_Some_0()) } else { diff --git a/src/controller_examples/zookeeper_controller/spec/reconciler.rs b/src/controller_examples/zookeeper_controller/spec/reconciler.rs index 719696492..c2044b9b4 100644 --- a/src/controller_examples/zookeeper_controller/spec/reconciler.rs +++ b/src/controller_examples/zookeeper_controller/spec/reconciler.rs @@ -109,7 +109,8 @@ pub open spec fn reconcile_core( // update let found_headless_service = unmarshal_headless_service_result.get_Ok_0(); let req_o = APIRequest::UpdateRequest(UpdateRequest { - key: make_headless_service_key(zk.object_ref()), + namespace: zk_namespace, + name: make_headless_service_name(zk_name), obj: update_headless_service(zk, found_headless_service).marshal(), }); let state_prime = ZookeeperReconcileState { @@ -209,7 +210,8 @@ pub open spec fn reconcile_core( // update let found_client_service = unmarshal_client_service_result.get_Ok_0(); let req_o = APIRequest::UpdateRequest(UpdateRequest { - key: make_client_service_key(zk.object_ref()), + namespace: zk_namespace, + name: make_client_service_name(zk_name), obj: update_client_service(zk, found_client_service).marshal(), }); let state_prime = ZookeeperReconcileState { @@ -309,7 +311,8 @@ pub open spec fn reconcile_core( // update let found_admin_server_service = unmarshal_admin_server_service_result.get_Ok_0(); let req_o = APIRequest::UpdateRequest(UpdateRequest { - key: make_admin_server_service_key(zk.object_ref()), + namespace: zk_namespace, + name: make_admin_server_service_name(zk_name), obj: update_admin_server_service(zk, found_admin_server_service).marshal(), }); let state_prime = ZookeeperReconcileState { @@ -409,7 +412,8 @@ pub open spec fn reconcile_core( // update let found_config_map = unmarshal_config_map_result.get_Ok_0(); let req_o = APIRequest::UpdateRequest(UpdateRequest { - key: make_config_map_key(zk.object_ref()), + namespace: zk_namespace, + name: make_config_map_name(zk_name), obj: update_config_map(zk, found_config_map).marshal(), }); let state_prime = ZookeeperReconcileState { @@ -634,7 +638,8 @@ pub open spec fn reconcile_core( // otherwise it might cause unsafe downscale. let latest_config_map_rv = state.latest_config_map_rv_opt.get_Some_0(); let req_o = APIRequest::UpdateRequest(UpdateRequest { - key: make_stateful_set_key(zk.object_ref()), + namespace: zk_namespace, + name: make_stateful_set_name(zk_name), obj: update_stateful_set(zk, found_stateful_set, latest_config_map_rv).marshal(), }); let state_prime = ZookeeperReconcileState { @@ -661,7 +666,8 @@ pub open spec fn reconcile_core( // otherwise it might cause unsafe downscale. let latest_config_map_rv = state.latest_config_map_rv_opt.get_Some_0(); let req_o = APIRequest::UpdateRequest(UpdateRequest { - key: make_stateful_set_key(zk.object_ref()), + namespace: zk_namespace, + name: make_stateful_set_name(zk_name), obj: update_stateful_set(zk, found_stateful_set, latest_config_map_rv).marshal(), }); let state_prime = ZookeeperReconcileState { diff --git a/src/kubernetes_api_objects/api_method.rs b/src/kubernetes_api_objects/api_method.rs index 9577549fe..039e3a17f 100644 --- a/src/kubernetes_api_objects/api_method.rs +++ b/src/kubernetes_api_objects/api_method.rs @@ -59,10 +59,21 @@ pub struct DeleteRequest { /// UpdateRequest replaces the existing obj with a new one. pub struct UpdateRequest { - pub key: ObjectRef, + pub namespace: StringView, + pub name: StringView, pub obj: DynamicObjectView, } +impl UpdateRequest { + pub open spec fn key(self) -> ObjectRef { + ObjectRef { + kind: self.obj.kind, + namespace: self.namespace, + name: self.name, + } + } +} + /// KubeAPIRequest represents API requests used in executable. /// /// kube-rs uses a generic type kube::api::Api as an api handle to send @@ -150,11 +161,8 @@ impl KubeAPIRequest { } }), KubeAPIRequest::UpdateRequest(update_req) => APIRequest::UpdateRequest(UpdateRequest { - key: ObjectRef { - kind: update_req.api_resource@.kind, - name: update_req.name@, - namespace: update_req.namespace@, - }, + name: update_req.name@, + namespace: update_req.namespace@, obj: update_req.obj@, }), } diff --git a/src/kubernetes_cluster/proof/builtin_controllers.rs b/src/kubernetes_cluster/proof/builtin_controllers.rs index 7b1ae58bd..e9a719f80 100644 --- a/src/kubernetes_cluster/proof/builtin_controllers.rs +++ b/src/kubernetes_cluster/proof/builtin_controllers.rs @@ -31,7 +31,7 @@ pub open spec fn every_update_msg_sets_owner_references_as( #[trigger] s.in_flight().contains(msg) && msg.dst.is_KubernetesAPI() && msg.content.is_update_request() - && msg.content.get_update_request().key == key + && msg.content.get_update_request().key() == key && msg.content.get_update_request().obj.kind == key.kind ==> requirements(msg.content.get_update_request().obj.metadata.owner_references) } diff --git a/src/kubernetes_cluster/spec/client/state_machine.rs b/src/kubernetes_cluster/spec/client/state_machine.rs index 4336abb63..1d2b47584 100644 --- a/src/kubernetes_cluster/spec/client/state_machine.rs +++ b/src/kubernetes_cluster/spec/client/state_machine.rs @@ -70,7 +70,7 @@ pub open spec fn update_custom_resource() -> ClientAction { }, transition: |input: ClientActionInput, s: ClientState| { let update_req_msg = Message::client_req_msg(Message::update_req_msg_content( - input.obj.object_ref(), input.obj, input.rest_id_allocator.allocate().1 + input.obj.metadata.namespace.get_Some_0(), input.obj.metadata.name.get_Some_0(), input.obj, input.rest_id_allocator.allocate().1 )); let s_prime = s; diff --git a/src/kubernetes_cluster/spec/kubernetes_api/state_machine.rs b/src/kubernetes_cluster/spec/kubernetes_api/state_machine.rs index 56952ef32..923c3195b 100644 --- a/src/kubernetes_cluster/spec/kubernetes_api/state_machine.rs +++ b/src/kubernetes_cluster/spec/kubernetes_api/state_machine.rs @@ -232,37 +232,33 @@ pub open spec fn validate_update_request(req: UpdateRequest, s: KubernetesAPISta if req.obj.metadata.name.is_None() { // Update fails because the name of the object is not provided Some(APIError::BadRequest) - } else if req.key.name != req.obj.metadata.name.get_Some_0() { + } else if req.name != req.obj.metadata.name.get_Some_0() { // Update fails because the name of the provided object // does not match the name sent on the request Some(APIError::BadRequest) } else if req.obj.metadata.namespace.is_Some() - && req.key.namespace != req.obj.metadata.namespace.get_Some_0() { + && req.namespace != req.obj.metadata.namespace.get_Some_0() { // Update fails because the namespace of the provided object // does not match the namespace sent on the request Some(APIError::BadRequest) - } else if req.obj.kind != req.key.kind { - // Update fails because the kind of the provided object - // does not match the kind sent on the request - Some(APIError::BadRequest) } else if !Self::spec_integrity_check(req.obj) { // Update fails because the spec of the provided object is not well formed // TODO: should the error be BadRequest? Some(APIError::BadRequest) - } else if !s.resources.contains_key(req.key) { + } else if !s.resources.contains_key(req.key()) { // Update fails because the object does not exist // TODO: check AllowCreateOnUpdate() to see whether to support create-on-update Some(APIError::ObjectNotFound) } else if req.obj.metadata.resource_version.is_None() - && !Self::allow_unconditional_update(req.key.kind) { + && !Self::allow_unconditional_update(req.key().kind) { // Update fails because the object does not provide a rv and unconditional update is not supported Some(APIError::Invalid) } else if req.obj.metadata.resource_version.is_Some() - && req.obj.metadata.resource_version != s.resources[req.key].metadata.resource_version { + && req.obj.metadata.resource_version != s.resources[req.key()].metadata.resource_version { // Update fails because the object has a wrong rv Some(APIError::Conflict) } else if req.obj.metadata.uid.is_Some() - && req.obj.metadata.uid != s.resources[req.key].metadata.uid { + && req.obj.metadata.uid != s.resources[req.key()].metadata.uid { // Update fails because the object has a wrong uid // TODO: double check the Error type Some(APIError::InternalError) @@ -277,14 +273,14 @@ pub open spec fn validate_update_request(req: UpdateRequest, s: KubernetesAPISta ) { // Update fails because the object has multiple controller owner references Some(APIError::Invalid) - } else if s.resources[req.key].metadata.deletion_timestamp.is_Some() + } else if s.resources[req.key()].metadata.deletion_timestamp.is_Some() && req.obj.metadata.finalizers.is_Some() // Short circuit: we don't need to reason about the set difference if the finalizers is None - && !req.obj.metadata.finalizers_as_set().subset_of(s.resources[req.key].metadata.finalizers_as_set()) { + && !req.obj.metadata.finalizers_as_set().subset_of(s.resources[req.key()].metadata.finalizers_as_set()) { // Update fails because the object is marked to be deleted but the update tries to add more finalizers Some(APIError::Forbidden) } else if !Self::state_validity_check(req.obj) { Some(APIError::Invalid) - } else if !Self::transition_validity_check(req.obj, s.resources[req.key]) { + } else if !Self::transition_validity_check(req.obj, s.resources[req.key()]) { Some(APIError::Invalid) } else { None @@ -292,8 +288,8 @@ pub open spec fn validate_update_request(req: UpdateRequest, s: KubernetesAPISta } pub open spec fn updated_object(req: UpdateRequest, s: KubernetesAPIState) -> DynamicObjectView { - let old_obj = s.resources[req.key]; - let updated_obj = req.obj.set_namespace(req.key.namespace) + let old_obj = s.resources[req.key()]; + let updated_obj = req.obj.set_namespace(req.namespace) // Update cannot change the rv; if rv is provided and inconsistent, validation fails. .set_resource_version(old_obj.metadata.resource_version.get_Some_0()) // Update cannot change the uid; if uid is provided and inconsistent, validation fails. @@ -318,11 +314,11 @@ pub open spec fn handle_update_request(msg: MsgType, s: KubernetesAPIState) - } else { // Update succeeds. let updated_obj = Self::updated_object(req, s); - if updated_obj == s.resources[req.key] { + if updated_obj == s.resources[req.key()] { // Update is a noop because there is nothing to update // so the resource version counter does not increase here, // and the resource version of this object remains the same. - let result = Ok(s.resources[req.key]); + let result = Ok(s.resources[req.key()]); let resp = Message::form_update_resp_msg(msg, result); (s, resp) } else { diff --git a/src/kubernetes_cluster/spec/message.rs b/src/kubernetes_cluster/spec/message.rs index 14ba967b4..30d067f6d 100644 --- a/src/kubernetes_cluster/spec/message.rs +++ b/src/kubernetes_cluster/spec/message.rs @@ -131,7 +131,7 @@ impl MessageContent { pub open spec fn is_update_request_with_key(self, key: ObjectRef) -> bool { &&& self.is_APIRequest() &&& self.get_APIRequest_0().is_UpdateRequest() - &&& self.get_APIRequest_0().get_UpdateRequest_0().key == key + &&& self.get_APIRequest_0().get_UpdateRequest_0().key() == key } pub open spec fn get_update_request(self) -> UpdateRequest @@ -335,9 +335,10 @@ pub open spec fn delete_req_msg_content(key: ObjectRef, req_id: RestId) -> Messa }), req_id) } -pub open spec fn update_req_msg_content(key: ObjectRef, obj: DynamicObjectView, req_id: RestId) -> MessageContent { +pub open spec fn update_req_msg_content(namespace: StringView, name: StringView, obj: DynamicObjectView, req_id: RestId) -> MessageContent { MessageContent::APIRequest(APIRequest::UpdateRequest(UpdateRequest{ - key: key, + namespace: namespace, + name: name, obj: obj, }), req_id) } From 7bfbdb6925d99c9e13b46908c0d3f4980d5bbf4f Mon Sep 17 00:00:00 2001 From: Xudong Sun Date: Wed, 20 Sep 2023 16:10:25 -0500 Subject: [PATCH 2/3] Remove todos Signed-off-by: Xudong Sun --- src/kubernetes_cluster/spec/kubernetes_api/state_machine.rs | 4 ---- 1 file changed, 4 deletions(-) diff --git a/src/kubernetes_cluster/spec/kubernetes_api/state_machine.rs b/src/kubernetes_cluster/spec/kubernetes_api/state_machine.rs index 923c3195b..c01dc2092 100644 --- a/src/kubernetes_cluster/spec/kubernetes_api/state_machine.rs +++ b/src/kubernetes_cluster/spec/kubernetes_api/state_machine.rs @@ -19,12 +19,8 @@ verus! { // // + Create and update should ignore the status fields provided by the object // -// + Make Create/Update/DeleteRequest consistent on whether to carry kind or not -// // + Support more operations like List // -// + Validation on uid, owner_references, finalizers -// // + Check kind-specific strategy like AllowUnconditionalUpdate() and AllowCreateOnUpdate() // // + Support graceful deletion From c3ce2dddbc759de6bfddb7a0dfb83c949f55ed55 Mon Sep 17 00:00:00 2001 From: Xudong Sun Date: Wed, 20 Sep 2023 16:37:06 -0500 Subject: [PATCH 3/3] Enlarge scaling test timeout Signed-off-by: Xudong Sun --- e2e/src/zookeeper_e2e.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/e2e/src/zookeeper_e2e.rs b/e2e/src/zookeeper_e2e.rs index 810f50053..f8c219c85 100644 --- a/e2e/src/zookeeper_e2e.rs +++ b/e2e/src/zookeeper_e2e.rs @@ -195,7 +195,7 @@ pub async fn desired_state_test(client: Client, zk_name: String) -> Result<(), E } pub async fn scaling_test(client: Client, zk_name: String) -> Result<(), Error> { - let timeout = Duration::from_secs(360); + let timeout = Duration::from_secs(600); let start = Instant::now(); let sts_api: Api = Api::default_namespaced(client.clone());