Support storage configuration for rabbitmq (#261)

Signed-off-by: Wenjie Ma <[email protected]>

deploy/rabbitmq/crd.yaml

@@ -21,6 +21,25 @@ spec:
           properties:
             spec:
               properties:
+                persistence:
+                  default:
+                    storageClassName: ~
+                    storage: 10Gi
+                  properties:
+                    storage:
+                      default: 10Gi
+                      description: "Quantity is a fixed-point representation of a number. It provides convenient marshaling/unmarshaling in JSON and YAML, in addition to String() and AsInt64() accessors.\n\nThe serialization format is:\n\n``` <quantity>        ::= <signedNumber><suffix>\n\n\t(Note that <suffix> may be empty, from the \"\" case in <decimalSI>.)\n\n<digit>           ::= 0 | 1 | ... | 9 <digits>          ::= <digit> | <digit><digits> <number>          ::= <digits> | <digits>.<digits> | <digits>. | .<digits> <sign>            ::= \"+\" | \"-\" <signedNumber>    ::= <number> | <sign><number> <suffix>          ::= <binarySI> | <decimalExponent> | <decimalSI> <binarySI>        ::= Ki | Mi | Gi | Ti | Pi | Ei\n\n\t(International System of units; See: http://physics.nist.gov/cuu/Units/binary.html)\n\n<decimalSI>       ::= m | \"\" | k | M | G | T | P | E\n\n\t(Note that 1024 = 1Ki but 1000 = 1k; I didn't choose the capitalization.)\n\n<decimalExponent> ::= \"e\" <signedNumber> | \"E\" <signedNumber> ```\n\nNo matter which of the three exponent forms is used, no quantity may represent a number greater than 2^63-1 in magnitude, nor may it have more than 3 decimal places. Numbers larger or more precise will be capped or rounded up. (E.g.: 0.1m will rounded up to 1m.) This may be extended in the future if we require larger or smaller quantities.\n\nWhen a Quantity is parsed from a string, it will remember the type of suffix it had, and will use the same type again when it is serialized.\n\nBefore serializing, Quantity will be put in \"canonical form\". This means that Exponent/suffix will be adjusted up or down (with a corresponding increase or decrease in Mantissa) such that:\n\n- No precision is lost - No fractional digits will be emitted - The exponent (or suffix) is as large as possible.\n\nThe sign will be omitted unless the number is negative.\n\nExamples:\n\n- 1.5 will be serialized as \"1500m\" - 1.5Gi will be serialized as \"1536Mi\"\n\nNote that the quantity will NEVER be internally represented by a floating point number. That is the whole point of this exercise.\n\nNon-canonical values will still parse as long as they are well formed, but will be re-emitted in their canonical form. (So always use canonical form, or don't diff.)\n\nThis format is intended to make it difficult to use these numbers without writing some sort of special handling code in the hopes that that will cause implementors to also use a fixed point implementation."
+                      type: string
+                      x-kubernetes-validations:
+                      - rule: "self == oldSelf"
+                        message: storage should not be changed
+                    storageClassName:
+                      nullable: true
+                      type: string
+                      x-kubernetes-validations:
+                      - rule: "self == oldSelf"
+                        message: storage class name should not be changed
+                  type: object
                 rabbitmqConfig:
                   nullable: true
                   properties:
@@ -49,4 +68,4 @@ spec:
           type: object
       served: true
       storage: true
-      subresources: {}
+      subresources: {}

deploy/rabbitmq/rabbitmq.yaml

@@ -8,3 +8,6 @@ spec:
   rabbitmqConfig:
     additionalConfig: |
       log.console.level = debug
+  persistence:
+    storage: 10Gi
+    storageClassName:

reference-controllers/rabbitmq-controller/src/statefulset.rs

@@ -86,8 +86,6 @@ fn persistent_volume_claim(rabbitmq: &RabbitmqCluster) ->Vec<corev1::PersistentV
     pvc
 }
 
-
-
 fn pod_template_spec(rabbitmq: &RabbitmqCluster, configmap_rv: String) -> corev1::PodTemplateSpec{
     let readiness_probe_port = "amqp".to_string(); // default one
     let volumes = vec![

src/controller_examples/rabbitmq_controller/exec/rabbitmqcluster.rs

@@ -17,7 +17,6 @@ pub struct RabbitmqCluster {
     inner: deps_hack::RabbitmqCluster
 }
 
-
 impl RabbitmqCluster {
     pub spec fn view(&self) -> RabbitmqClusterView;
 
@@ -124,7 +123,6 @@ pub struct RabbitmqClusterSpec {
     inner: deps_hack::RabbitmqClusterSpec,
 }
 
-
 impl RabbitmqClusterSpec {
     pub spec fn view(&self) -> RabbitmqClusterSpecView;
 
@@ -147,6 +145,14 @@ impl RabbitmqClusterSpec {
             None => None,
         }
     }
+
+    #[verifier(external_body)]
+    pub fn persistence(&self) -> (persistence: RabbitmqClusterPersistenceSpec)
+        ensures
+            persistence@ == self@.persistence,
+    {
+        RabbitmqClusterPersistenceSpec { inner: self.inner.persistence.clone() }
+    }
 }
 
 
@@ -171,5 +177,33 @@ impl RabbitmqConfig {
     }
 }
 
+#[verifier(external_body)]
+pub struct RabbitmqClusterPersistenceSpec {
+    inner: deps_hack::RabbitmqClusterPersistenceSpec,
+}
+
+impl RabbitmqClusterPersistenceSpec {
+    pub spec fn view(&self) -> RabbitmqClusterPersistenceSpecView;
+
+    #[verifier(external_body)]
+    pub fn storage(&self) -> (storage: String)
+        ensures
+            storage@ == self@.storage,
+    {
+        String::from_rust_string(self.inner.storage.clone().0)
+    }
+
+    #[verifier(external_body)]
+    pub fn storage_class_name(&self) -> (storage_class_name: Option<String>)
+        ensures
+            storage_class_name.is_Some() == self@.storage_class_name.is_Some(),
+            storage_class_name.is_Some() ==> storage_class_name.get_Some_0()@ == self@.storage_class_name.get_Some_0(),
+    {
+        match &self.inner.storage_class_name {
+            Some(n) => Some(String::from_rust_string(n.clone())),
+            None => None,
+        }
+    }
+}
 
 }

src/controller_examples/rabbitmq_controller/exec/reconciler.rs

@@ -1010,57 +1010,68 @@ fn make_stateful_set(rabbitmq: &RabbitmqCluster, config_map_rv: &String) -> (sta
         });
         // Set the templates used for creating the persistent volume claims attached to each pod
         stateful_set_spec.set_volume_claim_templates({ // TODO: Add PodManagementPolicy
-            let mut volume_claim_templates = Vec::new();
-            volume_claim_templates.push({
-                let mut pvc = PersistentVolumeClaim::default();
-                pvc.set_metadata({
-                    let mut metadata = ObjectMeta::default();
-                    metadata.set_name(new_strlit("persistence").to_string());
-                    metadata.set_namespace(rabbitmq.namespace().unwrap());
-                    metadata.set_labels({
-                        let mut labels = StringMap::empty();
-                        labels.insert(new_strlit("app").to_string(), rabbitmq.name().unwrap());
-                        labels
+            if rabbitmq.spec().persistence().storage().eq(&new_strlit("0Gi").to_string()) {
+                let empty_pvc = Vec::<PersistentVolumeClaim>::new();
+                proof {
+                    assert_seqs_equal!(
+                        [email protected]_values(|pvc: PersistentVolumeClaim| pvc@),
+                        rabbitmq_spec::make_stateful_set(rabbitmq@, config_map_rv@).spec.get_Some_0().volume_claim_templates.get_Some_0()
+                    );
+                }
+                empty_pvc
+            } else {
+                let mut volume_claim_templates = Vec::new();
+                volume_claim_templates.push({
+                    let mut pvc = PersistentVolumeClaim::default();
+                    pvc.set_metadata({
+                        let mut metadata = ObjectMeta::default();
+                        metadata.set_name(new_strlit("persistence").to_string());
+                        metadata.set_namespace(rabbitmq.namespace().unwrap());
+                        metadata.set_labels({
+                            let mut labels = StringMap::empty();
+                            labels.insert(new_strlit("app").to_string(), rabbitmq.name().unwrap());
+                            labels
+                        });
+                        metadata
                     });
-                    metadata
-                });
-                pvc.set_spec({
-                    let mut pvc_spec = PersistentVolumeClaimSpec::default();
-                    pvc_spec.set_access_modes({
-                        let mut access_modes = Vec::new();
-                        access_modes.push(new_strlit("ReadWriteOnce").to_string());
-
-                        proof {
-                            assert_seqs_equal!(
-                                [email protected]_values(|mode: String| mode@),
-                                rabbitmq_spec::make_stateful_set(rabbitmq@, config_map_rv@)
-                                    .spec.get_Some_0().volume_claim_templates.get_Some_0()[0]
-                                    .spec.get_Some_0().access_modes.get_Some_0()
-                            );
-                        }
+                    pvc.set_spec({
+                        let mut pvc_spec = PersistentVolumeClaimSpec::default();
+                        pvc_spec.set_access_modes({
+                            let mut access_modes = Vec::new();
+                            access_modes.push(new_strlit("ReadWriteOnce").to_string());
+                            proof {
+                                assert_seqs_equal!(
+                                    [email protected]_values(|mode: String| mode@),
+                                    rabbitmq_spec::make_stateful_set(rabbitmq@, config_map_rv@)
+                                        .spec.get_Some_0().volume_claim_templates.get_Some_0()[0]
+                                        .spec.get_Some_0().access_modes.get_Some_0()
+                                );
+                            }
 
-                        access_modes
-                    });
-                    pvc_spec.set_resources({
-                        let mut resources = ResourceRequirements::default();
-                        resources.set_requests({
-                            let mut requests = StringMap::empty();
-                            requests.insert(new_strlit("storage").to_string(), new_strlit("10Gi").to_string());
-                            requests
+                            access_modes
                         });
-                        resources
+                        pvc_spec.set_resources({
+                            let mut resources = ResourceRequirements::default();
+                            resources.set_requests({
+                                let mut requests = StringMap::empty();
+                                requests.insert(new_strlit("storage").to_string(), rabbitmq.spec().persistence().storage());
+                                requests
+                            });
+                            resources
+                        });
+                        pvc_spec.overwrite_storage_class_name(rabbitmq.spec().persistence().storage_class_name());
+                        pvc_spec
                     });
-                    pvc_spec
+                    pvc
                 });
-                pvc
-            });
-            proof {
-                assert_seqs_equal!(
-                    [email protected]_values(|pvc: PersistentVolumeClaim| pvc@),
-                    rabbitmq_spec::make_stateful_set(rabbitmq@, config_map_rv@).spec.get_Some_0().volume_claim_templates.get_Some_0()
-                );
+                proof {
+                    assert_seqs_equal!(
+                        [email protected]_values(|pvc: PersistentVolumeClaim| pvc@),
+                        rabbitmq_spec::make_stateful_set(rabbitmq@, config_map_rv@).spec.get_Some_0().volume_claim_templates.get_Some_0()
+                    );
+                }
+                volume_claim_templates
             }
-            volume_claim_templates
         });
         // Set management policy
         stateful_set_spec.set_pod_management_policy(new_strlit("Parallel").to_string());
@@ -1232,6 +1243,14 @@ fn make_rabbitmq_pod_spec(rabbitmq: &RabbitmqCluster) -> (pod_spec: PodSpec)
         });
         volume
     });
+    if rabbitmq.spec().persistence().storage().eq(&new_strlit("0Gi").to_string()) {
+        volumes.push({
+            let mut volume = Volume::default();
+            volume.set_name(new_strlit("persistence").to_string());
+            volume.set_empty_dir();
+            volume
+        });
+    }
     proof {
         assert_seqs_equal!(
             [email protected]_values(|vol: Volume| vol@),

src/controller_examples/rabbitmq_controller/spec/rabbitmqcluster.rs

@@ -110,12 +110,15 @@ impl ResourceView for RabbitmqClusterView {
 
     open spec fn transition_rule(new_obj: RabbitmqClusterView, old_obj: RabbitmqClusterView) -> bool {
         new_obj.spec.replicas >= old_obj.spec.replicas
+        && new_obj.spec.persistence.storage == old_obj.spec.persistence.storage
+        && new_obj.spec.persistence.storage_class_name == old_obj.spec.persistence.storage_class_name
     }
 
 }
 
 pub struct RabbitmqClusterSpecView {
     pub replicas: int,
+    pub persistence: RabbitmqClusterPersistenceSpecView,
     pub rabbitmq_config: Option<RabbitmqConfigView>,
 }
 
@@ -139,5 +142,10 @@ pub struct RabbitmqConfigView {
     pub env_config: Option<StringView>,
 }
 
+pub struct RabbitmqClusterPersistenceSpecView {
+    pub storage_class_name: Option<StringView>,
+    pub storage: StringView,
+}
+
 
 }

src/controller_examples/rabbitmq_controller/spec/reconciler.rs

@@ -675,22 +675,29 @@ pub open spec fn make_stateful_set(rabbitmq: RabbitmqClusterView, config_map_rv:
             )
             .set_spec(make_rabbitmq_pod_spec(rabbitmq))
         )
-        .set_volume_claim_templates(seq![
-            PersistentVolumeClaimView::default()
-                .set_metadata(ObjectMetaView::default()
-                    .set_name(new_strlit("persistence")@)
-                    .set_namespace(namespace)
-                    .set_labels(labels)
-                )
-                .set_spec(PersistentVolumeClaimSpecView::default()
-                    .set_access_modes(seq![new_strlit("ReadWriteOnce")@])
-                    .set_resources(ResourceRequirementsView::default()
-                        .set_requests(Map::empty()
-                            .insert(new_strlit("storage")@, new_strlit("10Gi")@)
+        .set_volume_claim_templates({
+            if rabbitmq.spec.persistence.storage == new_strlit("0Gi")@ {
+                seq![]
+            } else {
+                seq![
+                    PersistentVolumeClaimView::default()
+                        .set_metadata(ObjectMetaView::default()
+                            .set_name(new_strlit("persistence")@)
+                            .set_namespace(namespace)
+                            .set_labels(labels)
                         )
-                    )
-                )
-        ])
+                        .set_spec(PersistentVolumeClaimSpecView::default()
+                            .set_access_modes(seq![new_strlit("ReadWriteOnce")@])
+                            .set_resources(ResourceRequirementsView::default()
+                                .set_requests(Map::empty()
+                                    .insert(new_strlit("storage")@, rabbitmq.spec.persistence.storage)
+                                )
+                            )
+                            .overwrite_storage_class_name(rabbitmq.spec.persistence.storage_class_name)
+                        )
+                ]
+            }
+        })
         .set_pod_management_policy(new_strlit("Parallel")@);
 
     StatefulSetView::default().set_metadata(metadata).set_spec(spec)
@@ -832,7 +839,13 @@ pub open spec fn make_rabbitmq_pod_spec(rabbitmq: RabbitmqClusterView) -> PodSpe
                         .set_tcp_socket(TCPSocketActionView::default().set_port(5672))
                 )
         ])
-        .set_volumes(volumes)
+        .set_volumes({
+            if rabbitmq.spec.persistence.storage == new_strlit("0Gi")@ {
+                volumes.push(VolumeView::default().set_name(new_strlit("persistence")@))
+            } else {
+                volumes
+            }
+        })
 }
 
 }

src/deps_hack/src/lib.rs

@@ -107,10 +107,19 @@ pub struct ZookeeperConfig {
 #[kube(shortname = "rbmq", namespaced)]
 pub struct RabbitmqClusterSpec {
     pub replicas: i32,
+    #[serde(default = "default_persistence")]
+    pub persistence: RabbitmqClusterPersistenceSpec,
     #[serde(rename = "rabbitmqConfig")]
     pub rabbitmq_config: Option<RabbitmqConfig>,
 }
 
+pub fn default_persistence() -> RabbitmqClusterPersistenceSpec {
+    RabbitmqClusterPersistenceSpec {
+        storage: default_storage(),
+        storage_class_name: default_storage_class_name(),
+    }
+}
+
 #[derive(Debug, Clone, serde::Deserialize, serde::Serialize, schemars::JsonSchema)]
 pub struct RabbitmqConfig {
     #[serde(rename = "additionalConfig")]
@@ -121,6 +130,22 @@ pub struct RabbitmqConfig {
     pub env_config: Option<String>,
 }
 
+pub fn default_storage() -> k8s_openapi::apimachinery::pkg::api::resource::Quantity {
+    k8s_openapi::apimachinery::pkg::api::resource::Quantity("10Gi".to_string())
+}
+
+pub fn default_storage_class_name() -> Option<String> {
+    None
+}
+
+#[derive(Debug, Clone, serde::Deserialize, serde::Serialize, schemars::JsonSchema)]
+pub struct RabbitmqClusterPersistenceSpec {
+    #[serde(rename = "storageClassName", default = "default_storage_class_name")]
+    pub storage_class_name: Option<String>,
+    #[serde(default = "default_storage")]
+    pub storage: k8s_openapi::apimachinery::pkg::api::resource::Quantity,
+}
+
 #[derive(
     kube::CustomResource, Debug, Clone, serde::Deserialize, serde::Serialize, schemars::JsonSchema,
 )]