Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Remove kind from UpdateRequest #290

Merged
merged 3 commits into from
Sep 21, 2023
Merged

Remove kind from UpdateRequest #290

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
a6a41a4
Remove kind from UpdateRequest
marshtompsxd Sep 20, 2023
7bfbdb6
Remove todos
marshtompsxd Sep 20, 2023
c3ce2dd
Enlarge scaling test timeout
marshtompsxd Sep 20, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion e2e/src/zookeeper_e2e.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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<StatefulSet> = Api::default_namespaced(client.clone());

Expand Down
16 changes: 9 additions & 7 deletions src/controller_examples/rabbitmq_controller/spec/reconciler.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 {
Expand Down Expand Up @@ -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()
Expand Down Expand Up @@ -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 {
Expand Down
18 changes: 12 additions & 6 deletions src/controller_examples/zookeeper_controller/spec/reconciler.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 {
Expand Down Expand Up @@ -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 {
Expand Down Expand Up @@ -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 {
Expand Down Expand Up @@ -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 {
Expand Down Expand Up @@ -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 {
Expand All @@ -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 {
Expand Down
20 changes: 14 additions & 6 deletions src/kubernetes_api_objects/api_method.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -150,11 +161,8 @@ impl KubeAPIRequest {
}
}),
KubeAPIRequest::UpdateRequest(update_req) => APIRequest::UpdateRequest(UpdateRequest {
key: ObjectRef {
kind: [email protected],
name: update_req.name@,
namespace: update_req.namespace@,
},
name: update_req.name@,
namespace: update_req.namespace@,
obj: update_req.obj@,
}),
}
Expand Down
2 changes: 1 addition & 1 deletion src/kubernetes_cluster/proof/builtin_controllers.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)
}
Expand Down
2 changes: 1 addition & 1 deletion src/kubernetes_cluster/spec/client/state_machine.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -70,7 +70,7 @@ pub open spec fn update_custom_resource() -> ClientAction<E::Input, E::Output> {
},
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;
Expand Down
34 changes: 13 additions & 21 deletions src/kubernetes_cluster/spec/kubernetes_api/state_machine.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -232,37 +228,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)
Expand All @@ -277,23 +269,23 @@ 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
}
}

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.
Expand All @@ -318,11 +310,11 @@ pub open spec fn handle_update_request(msg: MsgType<E>, 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 {
Expand Down
7 changes: 4 additions & 3 deletions src/kubernetes_cluster/spec/message.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -131,7 +131,7 @@ impl<I, O> MessageContent<I, O> {
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
Expand Down Expand Up @@ -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<I, O> {
pub open spec fn update_req_msg_content(namespace: StringView, name: StringView, obj: DynamicObjectView, req_id: RestId) -> MessageContent<I, O> {
MessageContent::APIRequest(APIRequest::UpdateRequest(UpdateRequest{
key: key,
namespace: namespace,
name: name,
obj: obj,
}), req_id)
}
Expand Down
Loading