Skip to content

Commit

Permalink
Update admin server service
Browse files Browse the repository at this point in the history 
Signed-off-by: Xudong Sun <[email protected]>
  • Loading branch information
@marshtompsxd
marshtompsxd committed Sep 11, 2023
1 parent efa1dcf commit 33f32e4
Show file tree
Hide file tree
Showing 3 changed files with 255 additions and 21 deletions.
2 changes: 2 additions & 0 deletions src/controller_examples/zookeeper_controller/common/mod.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,9 @@ pub enum ZookeeperReconcileStep {
AfterGetClientService,
AfterCreateClientService,
AfterUpdateClientService,
AfterGetAdminServerService,
AfterCreateAdminServerService,
AfterUpdateAdminServerService,
AfterGetConfigMap,
AfterCreateConfigMap,
AfterUpdateConfigMap,
Expand Down
132 changes: 124 additions & 8 deletions src/controller_examples/zookeeper_controller/exec/reconciler.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -319,17 +319,102 @@ pub fn reconcile_core(
};
return (state_prime, None);
},
ZookeeperReconcileStep::AfterGetAdminServerService => {
if resp_o.is_some() && resp_o.as_ref().unwrap().is_k_response()
&& resp_o.as_ref().unwrap().as_k_response_ref().is_get_response() {
let get_admin_server_service_resp = resp_o.unwrap().into_k_response().into_get_response().res;
if get_admin_server_service_resp.is_ok() {
let unmarshal_admin_server_service_result = Service::from_dynamic_object(get_admin_server_service_resp.unwrap());
if unmarshal_admin_server_service_result.is_ok() {
// Update the admin_server service with the new port.
let found_admin_server_service = unmarshal_admin_server_service_result.unwrap();
if found_admin_server_service.spec().is_some() {
let new_admin_server_service = update_admin_server_service(zk, &found_admin_server_service);
let req_o = KubeAPIRequest::UpdateRequest(KubeUpdateRequest {
api_resource: Service::api_resource(),
name: make_admin_server_service_name(zk),
namespace: zk.metadata().namespace().unwrap(),
obj: new_admin_server_service.to_dynamic_object(),
});
let state_prime = ZookeeperReconcileState {
reconcile_step: ZookeeperReconcileStep::AfterUpdateAdminServerService,
..state
};
return (state_prime, Some(Request::KRequest(req_o)));
}
}
} else if get_admin_server_service_resp.unwrap_err().is_object_not_found() {
// Create the admin_server service since it doesn't exist yet.
let admin_server_service = make_admin_server_service(zk);
let req_o = KubeAPIRequest::CreateRequest(KubeCreateRequest {
api_resource: Service::api_resource(),
namespace: zk.metadata().namespace().unwrap(),
obj: admin_server_service.to_dynamic_object(),
});
let state_prime = ZookeeperReconcileState {
reconcile_step: ZookeeperReconcileStep::AfterCreateAdminServerService,
..state
};
return (state_prime, Some(Request::KRequest(req_o)));
}
}
let state_prime = ZookeeperReconcileState {
reconcile_step: ZookeeperReconcileStep::Error,
..state
};
return (state_prime, None);
},
ZookeeperReconcileStep::AfterCreateAdminServerService => {
let req_o = KubeAPIRequest::GetRequest(KubeGetRequest {
api_resource: ConfigMap::api_resource(),
name: make_config_map_name(zk),
namespace: zk.metadata().namespace().unwrap(),
});
if resp_o.is_some() && resp_o.as_ref().unwrap().is_k_response()
&& resp_o.as_ref().unwrap().as_k_response_ref().is_create_response() {
let create_admin_server_service_resp = resp_o.unwrap().into_k_response().into_create_response().res;
if create_admin_server_service_resp.is_ok() {
let unmarshal_admin_server_service_result = Service::from_dynamic_object(create_admin_server_service_resp.unwrap());
if unmarshal_admin_server_service_result.is_ok() {
let req_o = KubeAPIRequest::GetRequest(KubeGetRequest {
api_resource: ConfigMap::api_resource(),
name: make_config_map_name(zk),
namespace: zk.metadata().namespace().unwrap(),
});
let state_prime = ZookeeperReconcileState {
reconcile_step: ZookeeperReconcileStep::AfterGetConfigMap,
..state
};
return (state_prime, Some(Request::KRequest(req_o)));
}
}
}
let state_prime = ZookeeperReconcileState {
reconcile_step: ZookeeperReconcileStep::AfterGetConfigMap,
reconcile_step: ZookeeperReconcileStep::Error,
..state
};
return (state_prime, Some(Request::KRequest(req_o)));
return (state_prime, None);
},
ZookeeperReconcileStep::AfterUpdateAdminServerService => {
if resp_o.is_some() && resp_o.as_ref().unwrap().is_k_response()
&& resp_o.as_ref().unwrap().as_k_response_ref().is_update_response() {
let update_admin_server_service_resp = resp_o.unwrap().into_k_response().into_update_response().res;
if update_admin_server_service_resp.is_ok() {
let unmarshal_admin_server_service_result = Service::from_dynamic_object(update_admin_server_service_resp.unwrap());
if unmarshal_admin_server_service_result.is_ok() {
let req_o = KubeAPIRequest::GetRequest(KubeGetRequest {
api_resource: ConfigMap::api_resource(),
name: make_config_map_name(zk),
namespace: zk.metadata().namespace().unwrap(),
});
let state_prime = ZookeeperReconcileState {
reconcile_step: ZookeeperReconcileStep::AfterGetConfigMap,
..state
};
return (state_prime, Some(Request::KRequest(req_o)));
}
}
}
let state_prime = ZookeeperReconcileState {
reconcile_step: ZookeeperReconcileStep::Error,
..state
};
return (state_prime, None);
},
ZookeeperReconcileStep::AfterGetConfigMap => {
if resp_o.is_some() && resp_o.as_ref().unwrap().is_k_response()
Expand Down Expand Up @@ -775,6 +860,37 @@ fn make_client_service(zk: &ZookeeperCluster) -> (service: Service)
make_service(zk, make_client_service_name(zk), ports, true)
}

fn make_admin_server_service_name(zk: &ZookeeperCluster) -> (name: String)
requires
[email protected]_formed(),
ensures
name@ == zk_spec::make_admin_server_service_name([email protected]_Some_0()),
{
zk.metadata().name().unwrap().concat(new_strlit("-admin-server"))
}

fn update_admin_server_service(zk: &ZookeeperCluster, found_admin_server_service: &Service) -> (admin_server_service: Service)
requires
[email protected]_formed(),
[email protected]_Some(),
ensures
admin_server_service@ == zk_spec::update_admin_server_service(zk@, found_admin_server_service@),
{
let mut admin_server_service = found_admin_server_service.clone();
let made_admin_server_service = make_admin_server_service(zk);
admin_server_service.set_metadata({
let mut metadata = found_admin_server_service.metadata();
metadata.set_labels(made_admin_server_service.metadata().labels().unwrap());
metadata
});
admin_server_service.set_spec({
let mut spec = found_admin_server_service.spec().unwrap();
spec.set_ports(made_admin_server_service.spec().unwrap().ports().unwrap());
spec
});
admin_server_service
}

/// Admin-server Service is used for client to connect to admin server
fn make_admin_server_service(zk: &ZookeeperCluster) -> (service: Service)
requires
Expand All @@ -793,7 +909,7 @@ fn make_admin_server_service(zk: &ZookeeperCluster) -> (service: Service)
);
}

make_service(zk, zk.metadata().name().unwrap().concat(new_strlit("-admin-server")), ports, true)
make_service(zk, make_admin_server_service_name(zk), ports, true)
}

/// make_service constructs the Service object given the name, ports and cluster_ip
Expand Down
142 changes: 129 additions & 13 deletions src/controller_examples/zookeeper_controller/spec/reconciler.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -290,19 +290,105 @@ pub open spec fn reconcile_core(
(state_prime, None)
}
},
ZookeeperReconcileStep::AfterCreateAdminServerService => {
let req_o = APIRequest::GetRequest(GetRequest{
key: ObjectRef {
kind: ConfigMapView::kind(),
name: make_config_map_name(zk_name),
namespace: zk_namespace,
ZookeeperReconcileStep::AfterGetAdminServerService => {
if resp_o.is_Some() && resp.is_KResponse() && resp.get_KResponse_0().is_GetResponse() {
let get_admin_server_service_resp = resp.get_KResponse_0().get_GetResponse_0().res;
let unmarshal_admin_server_service_result = ServiceView::from_dynamic_object(get_admin_server_service_resp.get_Ok_0());
if get_admin_server_service_resp.is_Ok() {
if unmarshal_admin_server_service_result.is_Ok() && unmarshal_admin_server_service_result.get_Ok_0().spec.is_Some() {
// 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()),
obj: update_admin_server_service(zk, found_admin_server_service).to_dynamic_object(),
});
let state_prime = ZookeeperReconcileState {
reconcile_step: ZookeeperReconcileStep::AfterUpdateAdminServerService,
..state
};
(state_prime, Some(RequestView::KRequest(req_o)))
} else {
let state_prime = ZookeeperReconcileState {
reconcile_step: ZookeeperReconcileStep::Error,
..state
};
(state_prime, None)
}
} else if get_admin_server_service_resp.get_Err_0().is_ObjectNotFound() {
// create
let req_o = APIRequest::CreateRequest(CreateRequest {
namespace: zk_namespace,
obj: make_admin_server_service(zk).to_dynamic_object(),
});
let state_prime = ZookeeperReconcileState {
reconcile_step: ZookeeperReconcileStep::AfterCreateAdminServerService,
..state
};
(state_prime, Some(RequestView::KRequest(req_o)))
} else {
let state_prime = ZookeeperReconcileState {
reconcile_step: ZookeeperReconcileStep::Error,
..state
};
(state_prime, None)
}
});
let state_prime = ZookeeperReconcileState {
reconcile_step: ZookeeperReconcileStep::AfterGetConfigMap,
..state
};
(state_prime, Some(RequestView::KRequest(req_o)))
} else {
let state_prime = ZookeeperReconcileState {
reconcile_step: ZookeeperReconcileStep::Error,
..state
};
(state_prime, None)
}
},
ZookeeperReconcileStep::AfterCreateAdminServerService => {
let create_admin_server_service_resp = resp.get_KResponse_0().get_CreateResponse_0().res;
let unmarshal_admin_server_service_result = ServiceView::from_dynamic_object(create_admin_server_service_resp.get_Ok_0());
if resp_o.is_Some() && resp.is_KResponse() && resp.get_KResponse_0().is_CreateResponse()
&& create_admin_server_service_resp.is_Ok() && unmarshal_admin_server_service_result.is_Ok() {
let req_o = APIRequest::GetRequest(GetRequest{
key: ObjectRef {
kind: ConfigMapView::kind(),
name: make_config_map_name(zk_name),
namespace: zk_namespace,
}
});
let state_prime = ZookeeperReconcileState {
reconcile_step: ZookeeperReconcileStep::AfterGetConfigMap,
..state
};
(state_prime, Some(RequestView::KRequest(req_o)))
} else {
let state_prime = ZookeeperReconcileState {
reconcile_step: ZookeeperReconcileStep::Error,
..state
};
(state_prime, None)
}
},
ZookeeperReconcileStep::AfterUpdateAdminServerService => {
let update_admin_server_service_resp = resp.get_KResponse_0().get_UpdateResponse_0().res;
let unmarshal_admin_server_service_result = ServiceView::from_dynamic_object(update_admin_server_service_resp.get_Ok_0());
if resp_o.is_Some() && resp.is_KResponse() && resp.get_KResponse_0().is_UpdateResponse()
&& update_admin_server_service_resp.is_Ok() && unmarshal_admin_server_service_result.is_Ok() {
let req_o = APIRequest::GetRequest(GetRequest{
key: ObjectRef {
kind: ConfigMapView::kind(),
name: make_config_map_name(zk_name),
namespace: zk_namespace,
}
});
let state_prime = ZookeeperReconcileState {
reconcile_step: ZookeeperReconcileStep::AfterGetConfigMap,
..state
};
(state_prime, Some(RequestView::KRequest(req_o)))
} else {
let state_prime = ZookeeperReconcileState {
reconcile_step: ZookeeperReconcileStep::Error,
..state
};
(state_prime, None)
}
},
ZookeeperReconcileStep::AfterGetConfigMap => {
if resp_o.is_Some() && resp.is_KResponse() && resp.get_KResponse_0().is_GetResponse() {
Expand Down Expand Up @@ -709,13 +795,43 @@ pub open spec fn make_client_service(zk: ZookeeperClusterView) -> ServiceView
make_service(zk, make_client_service_name(zk.metadata.name.get_Some_0()), ports, true)
}

pub open spec fn make_admin_server_service_key(key: ObjectRef) -> ObjectRef
recommends
key.kind.is_CustomResourceKind(),
{
ObjectRef {
kind: ServiceView::kind(),
name: make_admin_server_service_name(key.name),
namespace: key.namespace,
}
}

pub open spec fn make_admin_server_service_name(zk_name: StringView) -> StringView {
zk_name + new_strlit("-admin-server")@
}

pub open spec fn update_admin_server_service(zk: ZookeeperClusterView, found_admin_server_service: ServiceView) -> ServiceView
recommends
zk.well_formed(),
{
found_admin_server_service
.set_metadata(
found_admin_server_service.metadata
.set_labels(make_admin_server_service(zk).metadata.labels.get_Some_0())
)
.set_spec(
found_admin_server_service.spec.get_Some_0()
.set_ports(make_admin_server_service(zk).spec.get_Some_0().ports.get_Some_0())
)
}

pub open spec fn make_admin_server_service(zk: ZookeeperClusterView) -> ServiceView
recommends
zk.well_formed(),
{
let ports = seq![ServicePortView::default().set_name(new_strlit("tcp-admin-server")@).set_port(zk.spec.admin_server_port)];

make_service(zk, zk.metadata.name.get_Some_0() + new_strlit("-admin-server")@, ports, true)
make_service(zk, make_admin_server_service_name(zk.metadata.name.get_Some_0()), ports, true)
}

pub open spec fn make_service(
Expand Down

0 comments on commit 33f32e4

Please sign in to comment.