Skip to content

Commit

Permalink
Refactor
Browse files Browse the repository at this point in the history 
Signed-off-by: Wenjie Ma <[email protected]>
  • Loading branch information
@euclidgame
euclidgame committed Sep 16, 2023
1 parent 1c883ae commit 4cb431a
Show file tree
Hide file tree
Showing 7 changed files with 653 additions and 192 deletions.
594 changes: 594 additions & 0 deletions crd.yml
View file

Large diffs are not rendered by default.

46 changes: 15 additions & 31 deletions deploy/rabbitmq/crd.yaml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -483,37 +483,6 @@ spec:
type: array
type: object
type: object
override:
default:
statefulSet: ~
description: Provides the ability to override the generated manifest of several child resources.
properties:
statefulSet:
description: Override configuration for the RabbitMQ StatefulSet.
nullable: true
properties:
spec:
description: StatefulSetSpec contains a subset of the fields included in k8s.io/api/apps/v1.StatefulSetSpec. Every field is made optional.
nullable: true
properties:
persistentVolumeClaimRetentionPolicy:
description: StatefulSetPersistentVolumeClaimRetentionPolicy describes the policy used for PVCs created from the StatefulSet VolumeClaimTemplates.
nullable: true
properties:
whenDeleted:
description: "WhenDeleted specifies what happens to PVCs created from StatefulSet VolumeClaimTemplates when the StatefulSet is deleted. The default policy of `Retain` causes PVCs to not be affected by StatefulSet deletion. The `Delete` policy causes those PVCs to be deleted."
type: string
whenScaled:
description: "WhenScaled specifies what happens to PVCs created from StatefulSet VolumeClaimTemplates when the StatefulSet is scaled down. The default policy of `Retain` causes PVCs to not be affected by a scaledown. The `Delete` policy causes the associated PVCs for any excess pods above the replica count to be deleted."
type: string
type: object
podManagementPolicy:
description: "podManagementPolicy controls how pods are created during initial scale up, when replacing pods on nodes, or when scaling down. The default policy is `OrderedReady`, where pods are created in increasing order (pod-0, then pod-1, etc) and the controller will wait until each pod is ready before continuing. When scaling down, the pods are removed in the opposite order. The alternative policy is `Parallel` which will create pods in parallel to match the desired scale without waiting, and on scale down will delete all pods at once."
nullable: true
type: string
type: object
type: object
type: object
persistence:
default:
storageClassName: ~
Expand All @@ -533,6 +502,21 @@ spec:
- rule: "self == oldSelf"
message: storage class name should not be changed
type: object
persistentVolumeClaimRetentionPolicy:
description: StatefulSetPersistentVolumeClaimRetentionPolicy describes the policy used for PVCs created from the StatefulSet VolumeClaimTemplates.
nullable: true
properties:
whenDeleted:
description: "WhenDeleted specifies what happens to PVCs created from StatefulSet VolumeClaimTemplates when the StatefulSet is deleted. The default policy of `Retain` causes PVCs to not be affected by StatefulSet deletion. The `Delete` policy causes those PVCs to be deleted."
type: string
whenScaled:
description: "WhenScaled specifies what happens to PVCs created from StatefulSet VolumeClaimTemplates when the StatefulSet is scaled down. The default policy of `Retain` causes PVCs to not be affected by a scaledown. The `Delete` policy causes the associated PVCs for any excess pods above the replica count to be deleted."
type: string
type: object
podManagementPolicy:
description: "podManagementPolicy controls how pods are created during initial scale up, when replacing pods on nodes, or when scaling down. The default policy is `OrderedReady`, where pods are created in increasing order (pod-0, then pod-1, etc) and the controller will wait until each pod is ready before continuing. When scaling down, the pods are removed in the opposite order. The alternative policy is `Parallel` which will create pods in parallel to match the desired scale without waiting, and on scale down will delete all pods at once."
nullable: true
type: string
rabbitmqConfig:
nullable: true
properties:
Expand Down
98 changes: 19 additions & 79 deletions src/controller_examples/rabbitmq_controller/exec/rabbitmqcluster.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -191,14 +191,29 @@ impl RabbitmqClusterSpec {
}

#[verifier(external_body)]
pub fn override_(&self) -> (override_: RabbitmqClusterOverrideSpec)
pub fn pod_management_policy(&self) -> (policy: Option<String>)
ensures
override_@ == self@.override_,
policy.is_Some() == self@.pod_management_policy.is_Some(),
policy.is_Some() ==> policy.get_Some_0()@ == self@.pod_management_policy.get_Some_0(),
{
RabbitmqClusterOverrideSpec { inner: self.inner.override_.clone() }
match &self.inner.pod_management_policy {
Some(s) => Some(String::from_rust_string(s.clone())),
None => None,
}
}
}

#[verifier(external_body)]
pub fn persistent_volume_claim_retention_policy(&self) -> (policy: Option<StatefulSetPersistentVolumeClaimRetentionPolicy>)
ensures
policy.is_Some() == self@.persistent_volume_claim_retention_policy.is_Some(),
policy.is_Some() ==> policy.get_Some_0()@ == self@.persistent_volume_claim_retention_policy.get_Some_0(),
{
match &self.inner.persistent_volume_claim_retention_policy {
Some(n) => Some(StatefulSetPersistentVolumeClaimRetentionPolicy::from_kube(n.clone())),
None => None,
}
}
}

#[verifier(external_body)]
pub struct RabbitmqConfig {
Expand Down Expand Up @@ -250,79 +265,4 @@ impl RabbitmqClusterPersistenceSpec {
}
}

#[verifier(external_body)]
pub struct RabbitmqClusterOverrideSpec {
inner: deps_hack::RabbitmqClusterOverrideSpec,
}

impl RabbitmqClusterOverrideSpec {
pub spec fn view(&self) -> RabbitmqClusterOverrideSpecView;

#[verifier(external_body)]
pub fn stateful_set(&self) -> (stateful_set: Option<RabbitmqOverrideStatefulSet>)
ensures
stateful_set.is_Some() == self@.stateful_set.is_Some(),
stateful_set.is_Some() ==> stateful_set.get_Some_0()@ == self@.stateful_set.get_Some_0(),
{
match &self.inner.stateful_set {
Some(sts) => Some(RabbitmqOverrideStatefulSet { inner: sts.clone() }),
None => None,
}
}
}

#[verifier(external_body)]
pub struct RabbitmqOverrideStatefulSet {
inner: deps_hack::RabbitmqOverrideStatefulSet,
}

impl RabbitmqOverrideStatefulSet {
pub spec fn view(&self) -> RabbitmqOverrideStatefulSetView;

#[verifier(external_body)]
pub fn spec(&self) -> (spec: Option<RabbitmqOverrideStatefulSetSpec>)
ensures
spec.is_Some() == self@.spec.is_Some(),
spec.is_Some() ==> spec.get_Some_0()@ == self@.spec.get_Some_0(),
{
match &self.inner.spec {
Some(s) => Some(RabbitmqOverrideStatefulSetSpec { inner: s.clone() }),
None => None,
}
}
}

#[verifier(external_body)]
pub struct RabbitmqOverrideStatefulSetSpec {
inner: deps_hack::RabbitmqOverrideStatefulSetSpec,
}

impl RabbitmqOverrideStatefulSetSpec {
pub spec fn view(&self) -> RabbitmqOverrideStatefulSetSpecView;

#[verifier(external_body)]
pub fn pod_management_policy(&self) -> (policy: Option<String>)
ensures
policy.is_Some() == self@.pod_management_policy.is_Some(),
policy.is_Some() ==> policy.get_Some_0()@ == self@.pod_management_policy.get_Some_0(),
{
match &self.inner.pod_management_policy {
Some(s) => Some(String::from_rust_string(s.clone())),
None => None,
}
}

#[verifier(external_body)]
pub fn persistent_volume_claim_retention_policy(&self) -> (policy: Option<StatefulSetPersistentVolumeClaimRetentionPolicy>)
ensures
policy.is_Some() == self@.persistent_volume_claim_retention_policy.is_Some(),
policy.is_Some() ==> policy.get_Some_0()@ == self@.persistent_volume_claim_retention_policy.get_Some_0(),
{
match &self.inner.persistent_volume_claim_retention_policy {
Some(n) => Some(StatefulSetPersistentVolumeClaimRetentionPolicy::from_kube(n.clone())),
None => None,
}
}
}

}
19 changes: 8 additions & 11 deletions src/controller_examples/rabbitmq_controller/exec/reconciler.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1090,17 +1090,14 @@ fn make_stateful_set(rabbitmq: &RabbitmqCluster, config_map_rv: &String) -> (sta
pod_template_spec
});
// Set management policy
stateful_set_spec.set_pod_management_policy(new_strlit("Parallel").to_string());
let override_sts_opt = rabbitmq.spec().override_().stateful_set();
if rabbitmq.spec().override_().stateful_set().is_some()
&& rabbitmq.spec().override_().stateful_set().unwrap().spec().is_some() {
let sts_spec = rabbitmq.spec().override_().stateful_set().unwrap().spec().unwrap();
if sts_spec.pod_management_policy().is_some() {
stateful_set_spec.set_pod_management_policy(sts_spec.pod_management_policy().unwrap());
}
if sts_spec.persistent_volume_claim_retention_policy().is_some() {
stateful_set_spec.set_pvc_retention_policy(sts_spec.persistent_volume_claim_retention_policy().unwrap());
}
if rabbitmq.spec().pod_management_policy().is_some() {
stateful_set_spec.set_pod_management_policy(rabbitmq.spec().pod_management_policy().unwrap());
} else {
stateful_set_spec.set_pod_management_policy(new_strlit("Parallel").to_string());
}

if rabbitmq.spec().persistent_volume_claim_retention_policy().is_some() {
stateful_set_spec.set_pvc_retention_policy(rabbitmq.spec().persistent_volume_claim_retention_policy().unwrap());
}
stateful_set_spec
});
Expand Down
29 changes: 2 additions & 27 deletions src/controller_examples/rabbitmq_controller/spec/rabbitmqcluster.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -123,23 +123,12 @@ pub struct RabbitmqClusterSpecView {
pub affinity: Option<AffinityView>,
pub tolerations: Option<Seq<TolerationView>>,
pub resources: Option<ResourceRequirementsView>,
pub override_: RabbitmqClusterOverrideSpecView,
pub pod_management_policy: Option<StringView>,
pub persistent_volume_claim_retention_policy: Option<StatefulSetPersistentVolumeClaimRetentionPolicyView>,
}

impl RabbitmqClusterSpecView {}

impl Marshalable for RabbitmqClusterSpecView {
spec fn marshal(self) -> Value;

spec fn unmarshal(value: Value) -> Result<Self, ParseDynamicObjectError>;

#[verifier(external_body)]
proof fn marshal_returns_non_null() {}

#[verifier(external_body)]
proof fn marshal_preserves_integrity() {}
}

pub struct RabbitmqConfigView {
pub additional_config: Option<StringView>,
pub advanced_config: Option<StringView>,
Expand All @@ -151,18 +140,4 @@ pub struct RabbitmqClusterPersistenceSpecView {
pub storage: StringView,
}

pub struct RabbitmqClusterOverrideSpecView {
pub stateful_set: Option<RabbitmqOverrideStatefulSetView>,
}

pub struct RabbitmqOverrideStatefulSetView {
pub spec: Option<RabbitmqOverrideStatefulSetSpecView>,
}

pub struct RabbitmqOverrideStatefulSetSpecView {
pub pod_management_policy: Option<StringView>,
pub persistent_volume_claim_retention_policy: Option<StatefulSetPersistentVolumeClaimRetentionPolicyView>,
}


}
12 changes: 3 additions & 9 deletions src/controller_examples/rabbitmq_controller/spec/reconciler.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -698,19 +698,13 @@ pub open spec fn make_stateful_set(rabbitmq: RabbitmqClusterView, config_map_rv:
}
}),
pod_management_policy: Some({
if rabbitmq.spec.override_.stateful_set.is_Some() && rabbitmq.spec.override_.stateful_set.get_Some_0().spec.is_Some()
&& rabbitmq.spec.override_.stateful_set.get_Some_0().spec.get_Some_0().pod_management_policy.is_Some() {
rabbitmq.spec.override_.stateful_set.get_Some_0().spec.get_Some_0().pod_management_policy.get_Some_0()
if rabbitmq.spec.pod_management_policy.is_Some() {
rabbitmq.spec.pod_management_policy.get_Some_0()
} else {
new_strlit("Parallel")@
}
}),
persistent_volume_claim_retention_policy:
if rabbitmq.spec.override_.stateful_set.is_Some() && rabbitmq.spec.override_.stateful_set.get_Some_0().spec.is_Some() {
rabbitmq.spec.override_.stateful_set.get_Some_0().spec.get_Some_0().persistent_volume_claim_retention_policy
} else {
None
},
persistent_volume_claim_retention_policy: rabbitmq.spec.persistent_volume_claim_retention_policy,
..StatefulSetSpecView::default()

};
Expand Down
47 changes: 12 additions & 35 deletions src/deps_hack/src/lib.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -114,8 +114,18 @@ pub struct RabbitmqClusterSpec {
pub affinity: Option<k8s_openapi::api::core::v1::Affinity>,
pub tolerations: Option<Vec<k8s_openapi::api::core::v1::Toleration>>,
pub resources: Option<k8s_openapi::api::core::v1::ResourceRequirements>,
#[serde(default, rename = "override")]
pub override_: RabbitmqClusterOverrideSpec,
/// podManagementPolicy controls how pods are created during initial scale up,
/// when replacing pods on nodes, or when scaling down. The default policy is
/// `OrderedReady`, where pods are created in increasing order (pod-0, then
/// pod-1, etc) and the controller will wait until each pod is ready before
/// continuing. When scaling down, the pods are removed in the opposite order.
/// The alternative policy is `Parallel` which will create pods in parallel
/// to match the desired scale without waiting, and on scale down will delete
/// all pods at once.
#[serde(rename = "podManagementPolicy")]
pub pod_management_policy: Option<String>,
#[serde(rename = "persistentVolumeClaimRetentionPolicy")]
pub persistent_volume_claim_retention_policy: Option<k8s_openapi::api::apps::v1::StatefulSetPersistentVolumeClaimRetentionPolicy>,
}

pub fn default_persistence() -> RabbitmqClusterPersistenceSpec {
Expand Down Expand Up @@ -147,39 +157,6 @@ pub struct RabbitmqClusterPersistenceSpec {
pub storage: k8s_openapi::apimachinery::pkg::api::resource::Quantity,
}

/// Provides the ability to override the generated manifest of several child resources.
#[derive(Default, Debug, Clone, serde::Deserialize, serde::Serialize, schemars::JsonSchema)]
pub struct RabbitmqClusterOverrideSpec {
/// Override configuration for the RabbitMQ StatefulSet.
#[serde(rename = "statefulSet")]
pub stateful_set: Option<RabbitmqOverrideStatefulSet>,
}

/// Allows for the manifest of the created StatefulSet to be overwritten with custom configuration.
#[derive(Debug, Clone, serde::Deserialize, serde::Serialize, schemars::JsonSchema)]
pub struct RabbitmqOverrideStatefulSet {
pub spec: Option<RabbitmqOverrideStatefulSetSpec>,
}

/// StatefulSetSpec contains a subset of the fields included in k8s.io/api/apps/v1.StatefulSetSpec.
/// Every field is made optional.
#[derive(Debug, Clone, serde::Deserialize, serde::Serialize, schemars::JsonSchema)]
pub struct RabbitmqOverrideStatefulSetSpec {

/// podManagementPolicy controls how pods are created during initial scale up,
/// when replacing pods on nodes, or when scaling down. The default policy is
/// `OrderedReady`, where pods are created in increasing order (pod-0, then
/// pod-1, etc) and the controller will wait until each pod is ready before
/// continuing. When scaling down, the pods are removed in the opposite order.
/// The alternative policy is `Parallel` which will create pods in parallel
/// to match the desired scale without waiting, and on scale down will delete
/// all pods at once.
#[serde(rename = "podManagementPolicy")]
pub pod_management_policy: Option<String>,
#[serde(rename = "persistentVolumeClaimRetentionPolicy")]
pub persistent_volume_claim_retention_policy: Option<k8s_openapi::api::apps::v1::StatefulSetPersistentVolumeClaimRetentionPolicy>,
}

#[derive(
kube::CustomResource, Debug, Clone, serde::Deserialize, serde::Serialize, schemars::JsonSchema,
)]
Expand Down

0 comments on commit 4cb431a

Please sign in to comment.