Support preconditions for Delete request (anvil-verifier#545)

This PR introduces `preconditions` of Kubernetes delete requests. The `preconditions` contain a uid and a resource version. When handling the delete request, the API server checks whether the object's uid and resource version match the ones provided by the request and returns `Conflict` error if not. Kubernetes implements this feature here: https://github.com/kubernetes/kubernetes/blob/v1.30.0/staging/src/k8s.io/apiserver/pkg/storage/interfaces.go#L140-L153. The `preconditions` is optional. Introducing `preconditions` mainly requires changes to the API server model (modeling the uid and resource version checking) and the shim layer (passing the `preconditions` to `kube`). This PR also fixes some of the lemmas that are broken due to `preconditions`. Having `preconditions` allows us to use more restrictive deletion. This is useful to ensure no interference between controllers that manage pods --- when a controller decides to delete a pod that the controller believes belongs to itself, the controller should pass to the `preconditions` the resource version of the pod it observes. When API server handles the delete request, if the pod happens to be owned by a different controller, then the deletion will be invalidated (because the resource version must have already changed since the controller's observation) so that the controller won't interfere with the new owner of the pod. --------- Signed-off-by: Xudong Sun <[email protected]>
xlab-uiuc · Sep 29, 2024 · 52e8753 · 52e8753
1 parent 9f6a0ff
commit 52e8753
Show file tree

Hide file tree

Showing 26 changed files with 237 additions and 52 deletions.
diff --git a/src/controller_examples/v_replica_set_controller/exec/reconciler.rs b/src/controller_examples/v_replica_set_controller/exec/reconciler.rs
@@ -138,6 +138,7 @@ pub fn reconcile_core(v_replica_set: &VReplicaSet, resp_o: Option<Response<Empty
                     api_resource: Pod::api_resource(),
                     name: pod_name_or_none.unwrap(),
                     namespace: namespace,
+                    preconditions: None,
                 });
                 let state_prime = VReplicaSetReconcileState {
                     reconcile_step: VReplicaSetReconcileStep::AfterDeletePod(diff - 1),
@@ -202,6 +203,7 @@ pub fn reconcile_core(v_replica_set: &VReplicaSet, resp_o: Option<Response<Empty
                     api_resource: Pod::api_resource(),
                     name: pod_name_or_none.unwrap(),
                     namespace: namespace,
+                    preconditions: None,
                 });
                 let state_prime = VReplicaSetReconcileState {
                     reconcile_step: VReplicaSetReconcileStep::AfterDeletePod(diff - 1),

diff --git a/src/controller_examples/v_replica_set_controller/model/reconciler.rs b/src/controller_examples/v_replica_set_controller/model/reconciler.rs
@@ -116,7 +116,8 @@ pub open spec fn reconcile_core(
                                         kind: PodView::kind(),
                                         name: pod_name_or_none.unwrap(),
                                         namespace: namespace,
-                                    }
+                                    },
+                                    preconditions: None,
                                 });
                                 let state_prime = VReplicaSetReconcileState {
                                     reconcile_step: VReplicaSetReconcileStep::AfterDeletePod((diff - 1) as usize),
@@ -182,7 +183,8 @@ pub open spec fn reconcile_core(
                                 kind: PodView::kind(),
                                 name: pod_name_or_none.unwrap(),
                                 namespace: namespace,
-                            }
+                            },
+                            preconditions: None,
                         });
                         let state_prime = VReplicaSetReconcileState {
                             reconcile_step: VReplicaSetReconcileStep::AfterDeletePod((diff - 1) as usize),

diff --git a/src/kubernetes_api_objects/exec/api_method.rs b/src/kubernetes_api_objects/exec/api_method.rs
@@ -1,12 +1,12 @@
 // Copyright 2022 VMware, Inc.
 // SPDX-License-Identifier: MIT
 use crate::kubernetes_api_objects::error::*;
-use crate::kubernetes_api_objects::exec::{api_resource::*, dynamic::*};
+use crate::kubernetes_api_objects::exec::{api_resource::*, dynamic::*, preconditions::*};
 use crate::kubernetes_api_objects::spec::{
     api_method::*,
     common::{Kind, ObjectRef},
 };
-use crate::vstd_ext::string_view::*;
+use crate::vstd_ext::{option_lib::*, string_view::*};
 use vstd::{prelude::*, string::*, view::*};
 
 use vstd::pervasive::unreached;
@@ -116,6 +116,7 @@ pub struct KubeDeleteRequest {
     pub api_resource: ApiResource,
     pub name: String,
     pub namespace: String,
+    pub preconditions: Option<Preconditions>,
 }
 
 impl KubeDeleteRequest {
@@ -133,7 +134,8 @@ impl View for KubeDeleteRequest {
                 kind: self.api_resource@.kind,
                 name: self.name@,
                 namespace: self.namespace@,
-            }
+            },
+            preconditions: option_view(self.preconditions),
         }
     }
 }
@@ -207,6 +209,7 @@ impl View for KubeAPIRequest {
     }
 }
 
+// TODO: replace it with option_view
 pub open spec fn opt_req_to_view(req: &Option<KubeAPIRequest>) -> Option<APIRequest> {
     match req {
         Some(req) => Some(req@),
@@ -519,6 +522,7 @@ impl KubeAPIResponse {
     }
 }
 
+// TODO: replace it with option_view
 pub open spec fn opt_resp_to_view(resp: &Option<KubeAPIResponse>) -> Option<APIResponse> {
     match resp {
         Some(resp) => Some(resp@),

diff --git a/src/kubernetes_api_objects/exec/mod.rs b/src/kubernetes_api_objects/exec/mod.rs
@@ -14,6 +14,7 @@ pub mod owner_reference;
 pub mod persistent_volume_claim;
 pub mod pod;
 pub mod pod_template_spec;
+pub mod preconditions;
 pub mod prelude;
 pub mod resource;
 pub mod resource_requirements;

diff --git a/src/kubernetes_api_objects/exec/preconditions.rs b/src/kubernetes_api_objects/exec/preconditions.rs
@@ -0,0 +1,59 @@
+// Copyright 2022 VMware, Inc.
+// SPDX-License-Identifier: MIT
+use crate::kubernetes_api_objects::exec::{object_meta::*, resource::*};
+use crate::kubernetes_api_objects::spec::preconditions::*;
+use crate::vstd_ext::string_view::*;
+use vstd::{prelude::*, string::*, view::*};
+
+verus! {
+
+#[verifier(external_body)]
+pub struct Preconditions {
+    inner: deps_hack::kube::api::Preconditions,
+}
+
+impl View for Preconditions {
+    type V = PreconditionsView;
+
+    spec fn view(&self) -> PreconditionsView;
+}
+
+impl std::clone::Clone for Preconditions {
+    #[verifier(external_body)]
+    fn clone(&self) -> (result: Preconditions)
+        ensures result@ == self@
+    {
+        Preconditions { inner: self.inner.clone() }
+    }
+}
+
+impl Preconditions {
+    #[verifier(external_body)]
+    pub fn default() -> (preconditions: Preconditions)
+        ensures preconditions@ == PreconditionsView::default(),
+    {
+        Preconditions { inner: deps_hack::kube::api::Preconditions::default() }
+    }
+
+    #[verifier(external_body)]
+    pub fn set_uid_from_object_meta(&mut self, object_meta: ObjectMeta)
+        ensures self@ == old(self)@.set_uid_from_object_meta(object_meta@),
+    {
+        self.inner.uid = object_meta.into_kube().uid;
+    }
+
+    #[verifier(external_body)]
+    pub fn set_resource_version_from_object_meta(&mut self, object_meta: ObjectMeta)
+        ensures self@ == old(self)@.set_resource_version_from_object_meta(object_meta@),
+    {
+        self.inner.resource_version = object_meta.into_kube().resource_version;
+    }
+
+    #[verifier(external)]
+    pub fn from_kube(inner: deps_hack::kube::api::Preconditions) -> Preconditions { Preconditions { inner: inner } }
+
+    #[verifier(external)]
+    pub fn into_kube(self) -> deps_hack::kube::api::Preconditions { self.inner }
+}
+
+}
diff --git a/src/kubernetes_api_objects/exec/prelude.rs b/src/kubernetes_api_objects/exec/prelude.rs
@@ -9,6 +9,7 @@ pub use crate::kubernetes_api_objects::exec::object_meta::*;
 pub use crate::kubernetes_api_objects::exec::owner_reference::*;
 pub use crate::kubernetes_api_objects::exec::persistent_volume_claim::*;
 pub use crate::kubernetes_api_objects::exec::pod::*;
+pub use crate::kubernetes_api_objects::exec::preconditions::*;
 pub use crate::kubernetes_api_objects::exec::resource::*;
 pub use crate::kubernetes_api_objects::exec::role::*;
 pub use crate::kubernetes_api_objects::exec::role_binding::*;

diff --git a/src/kubernetes_api_objects/spec/api_method.rs b/src/kubernetes_api_objects/spec/api_method.rs
@@ -4,13 +4,12 @@ use crate::kubernetes_api_objects::error::APIError;
 use crate::kubernetes_api_objects::spec::{
     common::{Kind, ObjectRef},
     dynamic::*,
+    preconditions::*,
 };
 use crate::vstd_ext::string_view::*;
 use vstd::string::*;
 use vstd::{prelude::*, view::*};
 
-use vstd::pervasive::unreached;
-
 verus! {
 
 /// APIRequest represents API requests sent to the Kubernetes API for specifications.
@@ -64,6 +63,7 @@ impl CreateRequest {
 
 pub struct DeleteRequest {
     pub key: ObjectRef,
+    pub preconditions: Option<PreconditionsView>,
 }
 
 /// UpdateRequest replaces the existing obj with a new one.

diff --git a/src/kubernetes_api_objects/spec/mod.rs b/src/kubernetes_api_objects/spec/mod.rs
@@ -14,6 +14,7 @@ pub mod owner_reference;
 pub mod persistent_volume_claim;
 pub mod pod;
 pub mod pod_template_spec;
+pub mod preconditions;
 pub mod prelude;
 pub mod resource;
 pub mod resource_requirements;

diff --git a/src/kubernetes_api_objects/spec/preconditions.rs b/src/kubernetes_api_objects/spec/preconditions.rs
@@ -0,0 +1,39 @@
+// Copyright 2022 VMware, Inc.
+// SPDX-License-Identifier: MIT
+use crate::kubernetes_api_objects::spec::{
+    common::{ResourceVersion, Uid},
+    object_meta::*,
+};
+use vstd::prelude::*;
+
+verus! {
+
+pub struct PreconditionsView {
+    pub uid: Option<Uid>,
+    pub resource_version: Option<ResourceVersion>,
+}
+
+impl PreconditionsView {
+    pub open spec fn default() -> PreconditionsView {
+        PreconditionsView {
+            uid: None,
+            resource_version: None,
+        }
+    }
+
+    pub open spec fn set_uid_from_object_meta(self, object_meta: ObjectMetaView) -> PreconditionsView {
+        PreconditionsView {
+            uid: object_meta.uid,
+            ..self
+        }
+    }
+
+    pub open spec fn set_resource_version_from_object_meta(self, object_meta: ObjectMetaView) -> PreconditionsView {
+        PreconditionsView {
+            resource_version: object_meta.resource_version,
+            ..self
+        }
+    }
+}
+
+}
diff --git a/src/kubernetes_api_objects/spec/prelude.rs b/src/kubernetes_api_objects/spec/prelude.rs
@@ -9,6 +9,7 @@ pub use crate::kubernetes_api_objects::spec::object_meta::*;
 pub use crate::kubernetes_api_objects::spec::owner_reference::*;
 pub use crate::kubernetes_api_objects::spec::persistent_volume_claim::*;
 pub use crate::kubernetes_api_objects::spec::pod::*;
+pub use crate::kubernetes_api_objects::spec::preconditions::*;
 pub use crate::kubernetes_api_objects::spec::resource::*;
 pub use crate::kubernetes_api_objects::spec::role::*;
 pub use crate::kubernetes_api_objects::spec::role_binding::*;

diff --git a/src/kubernetes_cluster/proof/builtin_controllers.rs b/src/kubernetes_cluster/proof/builtin_controllers.rs
@@ -168,7 +168,7 @@ pub proof fn lemma_eventually_objects_owner_references_satisfies(
     );
 
     assert forall |s, s_prime: Self| pre(s) && #[trigger] stronger_next(s, s_prime) && Self::builtin_controllers_next().forward(input)(s, s_prime) implies delete_msg_in_flight(s_prime) by {
-        let delete_req_msg = Message::built_in_controller_req_msg(Message::delete_req_msg_content(key, s.rest_id_allocator.allocate().1));
+        let delete_req_msg = Message::built_in_controller_req_msg(Message::delete_req_msg_content(key, s.rest_id_allocator.allocate().1, None));
         assert(s_prime.in_flight().contains(delete_req_msg));
     }
 
@@ -179,7 +179,7 @@ pub proof fn lemma_eventually_objects_owner_references_satisfies(
                 if i == input {
                     assert(Self::garbage_collector_deletion_enabled(key)(s));
                     let delete_req_msg = Message::built_in_controller_req_msg(Message::delete_req_msg_content(
-                        key, s.rest_id_allocator.allocate().1
+                        key, s.rest_id_allocator.allocate().1, None
                     ));
                     assert(s_prime.in_flight().contains(delete_req_msg));
                     assert(Self::exists_delete_request_msg_in_flight_with_key(key)(s_prime));

diff --git a/src/kubernetes_cluster/spec/builtin_controllers/garbage_collector.rs b/src/kubernetes_cluster/spec/builtin_controllers/garbage_collector.rs
@@ -56,8 +56,10 @@ pub open spec fn run_garbage_collector() -> BuiltinControllersAction<E::Input, E
             }
         },
         transition: |input: BuiltinControllersActionInput, s: ApiServerState| {
+            // Let's just use None preconditions for v1
+            // in v2, we set the proper preconditions
             let delete_req_msg = Message::built_in_controller_req_msg(Message::delete_req_msg_content(
-                input.key, input.rest_id_allocator.allocate().1
+                input.key, input.rest_id_allocator.allocate().1, None
             ));
             let s_prime = s;
             let output = BuiltinControllersActionOutput {

diff --git a/src/kubernetes_cluster/spec/client/state_machine.rs b/src/kubernetes_cluster/spec/client/state_machine.rs
@@ -48,7 +48,7 @@ pub open spec fn delete_custom_resource() -> ClientAction<E::Input, E::Output> {
         },
         transition: |input: ClientActionInput, s: ClientState| {
             let delete_req_msg = Message::client_req_msg(Message::delete_req_msg_content(
-                input.obj.object_ref(), input.rest_id_allocator.allocate().1
+                input.obj.object_ref(), input.rest_id_allocator.allocate().1, None
             ));
 
             let s_prime = s;

diff --git a/src/kubernetes_cluster/spec/message.rs b/src/kubernetes_cluster/spec/message.rs
@@ -3,7 +3,7 @@
 #![allow(unused_imports)]
 use crate::external_api::spec::*;
 use crate::kubernetes_api_objects::error::*;
-use crate::kubernetes_api_objects::spec::{api_method::*, common::*, dynamic::*};
+use crate::kubernetes_api_objects::spec::{api_method::*, common::*, dynamic::*, preconditions::*};
 use crate::vstd_ext::string_view::*;
 use vstd::{multiset::*, prelude::*};
 
@@ -373,9 +373,10 @@ pub open spec fn create_req_msg_content(namespace: StringView, obj: DynamicObjec
     }), req_id)
 }
 
-pub open spec fn delete_req_msg_content(key: ObjectRef, req_id: RestId) -> MessageContent<I, O> {
+pub open spec fn delete_req_msg_content(key: ObjectRef, req_id: RestId, preconditions: Option<PreconditionsView>) -> MessageContent<I, O> {
     MessageContent::APIRequest(APIRequest::DeleteRequest(DeleteRequest{
         key: key,
+        preconditions: preconditions,
     }), req_id)
 }
 

diff --git a/src/kubernetes_cluster/spec/pod_event/state_machine.rs b/src/kubernetes_cluster/spec/pod_event/state_machine.rs
@@ -44,7 +44,7 @@ pub open spec fn delete_pod() -> PodEventAction<E::Input, E::Output> {
         },
         transition: |input: PodEventActionInput, s: PodEventState| {
             let delete_req_msg = Message::pod_event_req_msg(Message::delete_req_msg_content(
-                input.pod.object_ref(), input.rest_id_allocator.allocate().1
+                input.pod.object_ref(), input.rest_id_allocator.allocate().1, None
             ));
 
             let s_prime = s;

diff --git a/src/shim_layer/controller_runtime.rs b/src/shim_layer/controller_runtime.rs
@@ -261,7 +261,12 @@ where
                                 &delete_req.namespace,
                                 delete_req.api_resource.as_kube_ref(),
                             );
-                            let dp = DeleteParams::default();
+                            let mut dp = DeleteParams::default();
+                            if delete_req.preconditions.is_some() {
+                                dp = dp.preconditions(
+                                    delete_req.preconditions.clone().unwrap().into_kube(),
+                                );
+                            }
                             let key = delete_req.key();
                             match api.delete(&delete_req.name, &dp).await {
                                 Err(err) => {

diff --git a/src/unit_tests/kubernetes_api_objects/api_method.rs b/src/unit_tests/kubernetes_api_objects/api_method.rs
@@ -83,6 +83,7 @@ pub fn test_deleterequest_key() {
         }),
         name: "name".to_string(),
         namespace: "namespace".to_string(),
+        preconditions: None,
     };
     assert_eq!(api_method.key(), "kind/namespace/name");
 }

diff --git a/src/v2/controllers/vreplicaset_controller/exec/reconciler.rs b/src/v2/controllers/vreplicaset_controller/exec/reconciler.rs
@@ -138,6 +138,7 @@ pub fn reconcile_core(v_replica_set: &VReplicaSet, resp_o: Option<Response<Empty
                     api_resource: Pod::api_resource(),
                     name: pod_name_or_none.unwrap(),
                     namespace: namespace,
+                    preconditions: None,
                 });
                 let state_prime = VReplicaSetReconcileState {
                     reconcile_step: VReplicaSetReconcileStep::AfterDeletePod(diff - 1),
@@ -202,6 +203,8 @@ pub fn reconcile_core(v_replica_set: &VReplicaSet, resp_o: Option<Response<Empty
                     api_resource: Pod::api_resource(),
                     name: pod_name_or_none.unwrap(),
                     namespace: namespace,
+                    // TODO: set the resource version to be the precondition
+                    preconditions: None,
                 });
                 let state_prime = VReplicaSetReconcileState {
                     reconcile_step: VReplicaSetReconcileStep::AfterDeletePod(diff - 1),

diff --git a/src/v2/controllers/vreplicaset_controller/model/reconciler.rs b/src/v2/controllers/vreplicaset_controller/model/reconciler.rs
@@ -116,7 +116,8 @@ pub open spec fn reconcile_core(
                                         kind: PodView::kind(),
                                         name: pod_name_or_none.unwrap(),
                                         namespace: namespace,
-                                    }
+                                    },
+                                    preconditions: None,
                                 });
                                 let state_prime = VReplicaSetReconcileState {
                                     reconcile_step: VReplicaSetReconcileStep::AfterDeletePod((diff - 1) as usize),
@@ -182,7 +183,8 @@ pub open spec fn reconcile_core(
                                 kind: PodView::kind(),
                                 name: pod_name_or_none.unwrap(),
                                 namespace: namespace,
-                            }
+                            },
+                            preconditions: None,
                         });
                         let state_prime = VReplicaSetReconcileState {
                             reconcile_step: VReplicaSetReconcileStep::AfterDeletePod((diff - 1) as usize),