From 1617723f385ce789f6d4d46458156f232fc60af3 Mon Sep 17 00:00:00 2001 From: Xudong Sun Date: Sun, 25 Feb 2024 18:52:17 -0600 Subject: [PATCH] Implement handler for deletion Signed-off-by: Xudong Sun --- src/executable_model/api_server.rs | 38 +++++++++++++++++-- src/executable_model/common.rs | 12 ++++++ src/kubernetes_api_objects/exec/api_method.rs | 2 - .../spec/api_server/state_machine.rs | 15 ++++++-- 4 files changed, 59 insertions(+), 8 deletions(-) diff --git a/src/executable_model/api_server.rs b/src/executable_model/api_server.rs index 135a4c8de..f5e03f555 100644 --- a/src/executable_model/api_server.rs +++ b/src/executable_model/api_server.rs @@ -147,15 +147,15 @@ fn object_transition_validity_check(obj: &DynamicObject, old_obj: &DynamicObject pub fn handle_get_request(req: &KubeGetRequest, s: &ApiServerState) -> (ret: KubeGetResponse) ensures ret@ == model::handle_get_request(req@, s@) { - let object_ref = KubeObjectRef { + let req_key = KubeObjectRef { kind: req.api_resource.kind(), name: req.name.clone(), namespace: req.namespace.clone(), }; - if !s.resources.contains_key(&object_ref) { + if !s.resources.contains_key(&req_key) { KubeGetResponse{res: Err(APIError::ObjectNotFound)} } else { - KubeGetResponse{res: Ok(s.resources.get(&object_ref).unwrap())} + KubeGetResponse{res: Ok(s.resources.get(&req_key).unwrap())} } } @@ -223,6 +223,38 @@ pub fn handle_create_request(req: &KubeCreateRequest, s: &mut ApiServerState) -> } } +pub fn handle_delete_request(req: &KubeDeleteRequest, s: &mut ApiServerState) -> (ret: KubeDeleteResponse) + requires old(s).resource_version_counter < i64::MAX // No integer overflow + ensures (s@, ret@) == model::handle_delete_request(req@, old(s)@) +{ + let req_key = KubeObjectRef { + kind: req.api_resource.kind(), + name: req.name.clone(), + namespace: req.namespace.clone(), + }; + if !s.resources.contains_key(&req_key) { + KubeDeleteResponse{res: Err(APIError::ObjectNotFound)} + } else { + let mut obj = s.resources.get(&req_key).unwrap(); + if obj.metadata().finalizers().is_some() && obj.metadata().finalizers().unwrap().len() > 0 { + if obj.metadata().has_deletion_timestamp() { + KubeDeleteResponse{res: Ok(())} + } else { + obj.set_current_deletion_timestamp(); + obj.set_resource_version(s.resource_version_counter); + let stamped_obj_with_new_rv = obj; // This renaming is just to stay consistent with the model + s.resources.insert(req_key, stamped_obj_with_new_rv); + s.resource_version_counter = s.resource_version_counter + 1; + KubeDeleteResponse{res: Ok(())} + } + } else { + s.resources.remove(&req_key); + s.resource_version_counter = s.resource_version_counter + 1; + KubeDeleteResponse{res: Ok(())} + } + } +} + fn allow_unconditional_update(kind: &Kind) -> (ret: bool) ensures ret == model::allow_unconditional_update(*kind) { diff --git a/src/executable_model/common.rs b/src/executable_model/common.rs index 08f54d6c8..37882f9d9 100644 --- a/src/executable_model/common.rs +++ b/src/executable_model/common.rs @@ -256,6 +256,18 @@ impl DynamicObject { self.as_kube_mut_ref().metadata.deletion_timestamp = other.as_kube_ref().metadata.deletion_timestamp.clone(); } + + // This function sets the deletion timestamp to the current time. + // This seems a bit inconsistent with the model's behavior which + // always sets it to the return value of deletion_timestamp(). + // However, this function is actually closer to Kubernetes' real behavior. + #[verifier(external_body)] + pub fn set_current_deletion_timestamp(&mut self) + ensures self@ == old(self)@.set_deletion_timestamp(model::deletion_timestamp()), + { + self.as_kube_mut_ref().metadata.deletion_timestamp = Some(deps_hack::k8s_openapi::apimachinery::pkg::apis::meta::v1::Time(deps_hack::chrono::Utc::now())); + } + #[verifier(external_body)] pub fn eq(&self, other: &DynamicObject) -> (ret: bool) ensures ret == (self@ == other@) diff --git a/src/kubernetes_api_objects/exec/api_method.rs b/src/kubernetes_api_objects/exec/api_method.rs index 74fabd75c..ccbad8077 100644 --- a/src/kubernetes_api_objects/exec/api_method.rs +++ b/src/kubernetes_api_objects/exec/api_method.rs @@ -62,8 +62,6 @@ impl View for KubeGetRequest { } /// KubeListRequest has the namespace to instantiate an Api. -/// -/// Note that the kind is indicated by the upper layer Kube{ObjectKind}Request. pub struct KubeListRequest { pub api_resource: ApiResource, diff --git a/src/kubernetes_cluster/spec/api_server/state_machine.rs b/src/kubernetes_cluster/spec/api_server/state_machine.rs index c2459e5d0..42b62957d 100644 --- a/src/kubernetes_cluster/spec/api_server/state_machine.rs +++ b/src/kubernetes_cluster/spec/api_server/state_machine.rs @@ -228,6 +228,14 @@ pub open spec fn handle_create_request(req: CreateRequest } } +// Here we make a compromise when modeling the behavior of setting +// deletion timestamp to each object that is deemed to be deleted. +// The real Kubernetes' behavior uses the current timestamp as the +// deletion timestamp, but we only use an opaque string here. +// This is fine because the request handling logic we want to model +// only cares whether the object has a deletion timestamp or not. +// By using this closed deletion_timestamp() function, we make the +// modeling and proof much easier compared to modelling the real clock. pub closed spec fn deletion_timestamp() -> StringView; pub open spec fn handle_delete_request(req: DeleteRequest, s: ApiServerState) -> (ApiServerState, DeleteResponse) { @@ -240,11 +248,12 @@ pub open spec fn handle_delete_request(req: DeleteRequest, s: ApiServerState) -> if obj.metadata.finalizers.is_Some() && obj.metadata.finalizers.get_Some_0().len() > 0 { // With the finalizer(s) in the object, we cannot immediately delete it from the key-value store. // Instead, we set the deletion timestamp of this object. - let stamped_obj = obj.set_deletion_timestamp(deletion_timestamp()); - if stamped_obj == obj { + // If the object already has a deletion timestamp, then skip. + if obj.metadata.deletion_timestamp.is_Some() { (s, DeleteResponse{res: Ok(())}) } else { - let stamped_obj_with_new_rv = stamped_obj.set_resource_version(s.resource_version_counter); + let stamped_obj_with_new_rv = obj.set_deletion_timestamp(deletion_timestamp()) + .set_resource_version(s.resource_version_counter); (ApiServerState { // Here we use req.key, instead of stamped_obj.object_ref(), to insert to the map. // This is intended because using stamped_obj.object_ref() will require us to use