Skip to content

Commit

Permalink
Make the action of issuing lib req and call lib atomic
Browse files Browse the repository at this point in the history 
Signed-off-by: Wenjie Ma <[email protected]>
  • Loading branch information
@euclidgame
euclidgame committed Jul 23, 2023
1 parent 9c1b7cd commit c472fd4
Show file tree
Hide file tree
Showing 4 changed files with 46 additions and 79 deletions.
3 changes: 0 additions & 3 deletions src/kubernetes_cluster/proof/controller_runtime.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -84,19 +84,16 @@ pub open spec fn at_expected_reconcile_states<K: ResourceView, R: Reconciler<K>>

pub open spec fn pending_k8s_api_req_msg<K: ResourceView, R: Reconciler<K>>(s: State<K, R>, key: ObjectRef) -> bool {
s.reconcile_state_of(key).pending_req_msg.is_Some()
&& s.reconcile_state_of(key).pending_lib_req.is_None()
&& s.reconcile_state_of(key).lib_response.is_None()
}

pub open spec fn pending_k8s_api_req_msg_is<K: ResourceView, R: Reconciler<K>>(s: State<K, R>, key: ObjectRef, req: Message) -> bool {
s.reconcile_state_of(key).pending_req_msg == Option::Some(req)
&& s.reconcile_state_of(key).pending_lib_req.is_None()
&& s.reconcile_state_of(key).lib_response.is_None()
}

pub open spec fn no_pending_request<K: ResourceView, R: Reconciler<K>>(s: State<K, R>, key: ObjectRef) -> bool {
s.reconcile_state_of(key).pending_req_msg.is_None()
&& s.reconcile_state_of(key).pending_lib_req.is_None()
&& s.reconcile_state_of(key).lib_response.is_None()
}

Expand Down
1 change: 0 additions & 1 deletion src/kubernetes_cluster/proof/controller_runtime_safety.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -230,7 +230,6 @@ pub open spec fn req_in_flight_or_pending_at_controller<K: ResourceView, R: Reco
|| exists |cr_key: ObjectRef| (
#[trigger] s.reconcile_state_contains(cr_key)
&& pending_k8s_api_req_msg_is(s, cr_key, req_msg)
&& s.reconcile_state_of(cr_key).pending_lib_req.is_None()
&& s.reconcile_state_of(cr_key).lib_response.is_None()
))
}
Expand Down
8 changes: 2 additions & 6 deletions src/kubernetes_cluster/spec/controller/common.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -17,13 +17,9 @@ pub struct ControllerState<K: ResourceView, R: Reconciler<K>> {

pub struct OngoingReconcile<K: ResourceView, R: Reconciler<K>> {
pub triggering_cr: K,
// Use two fields for pending k8s api request and pending external library result separately.
// Such design is not very reasonable because it doesn't make it apparent that the two fields
// are mutually exclusive, i.e., only one of them can be non-empty at some point.
// But this is fine, since we can describe the state as one of them is Option::Some(...) and
// the other is Option::None.
// pending_req_msg:
// lib_response:
pub pending_req_msg: Option<Message>,
pub pending_lib_req: Option<R::I>,
pub lib_response: Option<R::O>,
pub local_state: R::T,
}
Expand Down
113 changes: 44 additions & 69 deletions src/kubernetes_cluster/spec/controller/controller_runtime.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -25,7 +25,6 @@ pub open spec fn run_scheduled_reconcile<K: ResourceView, R: Reconciler<K>>() ->
let initialized_ongoing_reconcile = OngoingReconcile {
triggering_cr: s.scheduled_reconciles[cr_key],
pending_req_msg: Option::None,
pending_lib_req: Option::None,
lib_response: Option::None,
local_state: R::reconcile_init_state(),
};
Expand All @@ -52,29 +51,21 @@ pub open spec fn continue_reconcile<K: ResourceView, R: Reconciler<K>>() -> Cont
&&& !R::reconcile_error(s.ongoing_reconciles[cr_key].local_state)
// Split cases:
// (1) there is a pending request which is destined for kubernetes api;
// (2) there is a pending request which is destined for external library and no response;
// (3) there is a pending request which is destined for external library and a corresponding response;
// (4) there is no pending request;
// The four cases don't overlap each other, and we must make them mutually exclusive in the
// (3) there is no pending request which is destined for kubernetes api and there is a external response;
// (4) there is no pending request or external response;
// The three cases don't overlap each other, and we must make them mutually exclusive in the
// precondition, i.e., there should not be a state which satifies the precondition but fits for more
// than one case of the four.
// than one case of the three.
// Note that if there is no pending request destined for kubernetes api, we have to require that
// the recv field of input is empty and exclude the case where pending_lib_req is empty and
// lib_response is not.
// the recv field of input is empty.
&&& if s.ongoing_reconciles[cr_key].pending_req_msg.is_Some() {
&&& s.ongoing_reconciles[cr_key].lib_response.is_None() // The response from external library should have been consumed if ever exists
&&& s.ongoing_reconciles[cr_key].pending_lib_req.is_None()
&&& input.recv.is_Some()
&&& input.recv.get_Some_0().content.is_APIResponse()
&&& resp_msg_matches_req_msg(input.recv.get_Some_0(), s.ongoing_reconciles[cr_key].pending_req_msg.get_Some_0())
} else {
// We should not get response from other part of the GSM for this case.
&&& input.recv.is_None()
&&& if s.ongoing_reconciles[cr_key].pending_lib_req.is_None() {
s.ongoing_reconciles[cr_key].lib_response.is_None()
} else {
true
}
}
} else {
false
Expand All @@ -90,69 +81,53 @@ pub open spec fn continue_reconcile<K: ResourceView, R: Reconciler<K>>() -> Cont
} else {
Option::None
};
if reconcile_state.pending_lib_req.is_Some() && reconcile_state.lib_response.is_None() {
// This is the only case we should call the external Library.
// We first make it do nothing here.
let (local_state_prime, req_o) = R::reconcile_core(reconcile_state.triggering_cr, resp_o, reconcile_state.local_state);
if req_o.is_Some() {
match req_o.get_Some_0() {
RequestView::KRequest(req) => {
let (rest_id_allocator_prime, pending_req_msg)
= (input.rest_id_allocator.allocate().0, Option::Some(controller_req_msg(req, input.rest_id_allocator.allocate().1)));
let reconcile_state_prime = OngoingReconcile {
pending_req_msg: pending_req_msg,
lib_response: Option::None,
local_state: local_state_prime,
..reconcile_state
};
let s_prime = ControllerState {
ongoing_reconciles: s.ongoing_reconciles.insert(cr_key, reconcile_state_prime),
..s
};
(s_prime, (Multiset::singleton(pending_req_msg.get_Some_0()), rest_id_allocator_prime))
},
RequestView::ExternalRequest(req) => {
// Call the external library first.

// Then update the state.
let reconcile_state_prime = OngoingReconcile {
pending_req_msg: Option::None,
lib_response: Option::None, // TODO: update this field after add the library as a generic
local_state: local_state_prime,
..reconcile_state
};
let s_prime = ControllerState {
ongoing_reconciles: s.ongoing_reconciles.insert(cr_key, reconcile_state_prime),
..s
};
(s_prime, (Multiset::empty(), input.rest_id_allocator.allocate().0))
}
}
} else {
let reconcile_state_prime = OngoingReconcile {
pending_lib_req: Option::None,
lib_response: Option::None, // Should be updated
pending_req_msg: Option::None,
lib_response: Option::None,
local_state: local_state_prime,
..reconcile_state
};
let s_prime = ControllerState {
ongoing_reconciles: s.ongoing_reconciles.insert(cr_key, reconcile_state_prime),
..s
};
(s_prime, (Multiset::empty(), input.rest_id_allocator.allocate().0))
} else {
// Otherwise, we call the reconcile_core.
let (local_state_prime, req_o) = R::reconcile_core(reconcile_state.triggering_cr, resp_o, reconcile_state.local_state);
if req_o.is_Some() {
match req_o.get_Some_0() {
RequestView::KRequest(req) => {
let (rest_id_allocator_prime, pending_req_msg)
= (input.rest_id_allocator.allocate().0, Option::Some(controller_req_msg(req, input.rest_id_allocator.allocate().1)));
let reconcile_state_prime = OngoingReconcile {
pending_req_msg: pending_req_msg,
pending_lib_req: Option::None,
lib_response: Option::None,
local_state: local_state_prime,
..reconcile_state
};
let s_prime = ControllerState {
ongoing_reconciles: s.ongoing_reconciles.insert(cr_key, reconcile_state_prime),
..s
};
(s_prime, (Multiset::singleton(pending_req_msg.get_Some_0()), rest_id_allocator_prime))
},
RequestView::ExternalRequest(req) => {
let reconcile_state_prime = OngoingReconcile {
pending_req_msg: Option::None,
pending_lib_req: Option::Some(req),
lib_response: Option::None,
local_state: local_state_prime,
..reconcile_state
};
let s_prime = ControllerState {
ongoing_reconciles: s.ongoing_reconciles.insert(cr_key, reconcile_state_prime),
..s
};
(s_prime, (Multiset::empty(), input.rest_id_allocator.allocate().0))
}
}
} else {
let reconcile_state_prime = OngoingReconcile {
pending_req_msg: Option::None,
pending_lib_req: Option::None,
lib_response: Option::None,
local_state: local_state_prime,
..reconcile_state
};
let s_prime = ControllerState {
ongoing_reconciles: s.ongoing_reconciles.insert(cr_key, reconcile_state_prime),
..s
};
(s_prime, (Multiset::empty(), input.rest_id_allocator.allocate().0))
}
}
}
}
Expand Down

0 comments on commit c472fd4

Please sign in to comment.