Add resources to FluentBit (#194)

The new field `resources` allows the user to specify CPU/memory allocation to the running fluent bit process. Adding the new field doesn't affect the control flow and only requires small changes to the code base, mainly for defining new wrapper and ghost types. --------- Signed-off-by: Xudong Sun <[email protected]>
anvil-verifier · Aug 4, 2023 · 6d9d2e2 · 6d9d2e2
1 parent 4494f77
commit 6d9d2e2
Show file tree

Hide file tree

Showing 10 changed files with 76 additions and 5 deletions.
diff --git a/deploy/fluent/crd.yaml b/deploy/fluent/crd.yaml
@@ -25,6 +25,35 @@ spec:
                   type: string
                 parsersConfig:
                   type: string
+                resources:
+                  default: {}
+                  description: ResourceRequirements describes the compute resource requirements.
+                  properties:
+                    claims:
+                      description: "Claims lists the names of resources, defined in spec.resourceClaims, that are used by this container.\n\nThis is an alpha field and requires enabling the DynamicResourceAllocation feature gate.\n\nThis field is immutable."
+                      items:
+                        description: ResourceClaim references one entry in PodSpec.ResourceClaims.
+                        properties:
+                          name:
+                            description: Name must match the name of one entry in pod.spec.resourceClaims of the Pod where this field is used. It makes that resource available inside a container.
+                            type: string
+                        required:
+                          - name
+                        type: object
+                      type: array
+                    limits:
+                      additionalProperties:
+                        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
+                      description: "Limits describes the maximum amount of compute resources allowed. More info: https://kubernetes.io/docs/concepts/configuration/manage-resources-containers/"
+                      type: object
+                    requests:
+                      additionalProperties:
+                        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
+                      description: "Requests describes the minimum amount of compute resources required. If Requests is omitted for a container, it defaults to Limits if that is explicitly specified, otherwise to an implementation-defined value. More info: https://kubernetes.io/docs/concepts/configuration/manage-resources-containers/"
+                      type: object
+                  type: object
               required:
                 - fluentBitConfig
                 - parsersConfig

diff --git a/src/controller_examples/fluent_controller/exec/fluentbit.rs b/src/controller_examples/fluent_controller/exec/fluentbit.rs
@@ -4,6 +4,7 @@ use crate::fluent_controller::spec::fluentbit::*;
 use crate::kubernetes_api_objects::error::ParseDynamicObjectError;
 use crate::kubernetes_api_objects::{
     api_resource::*, common::*, dynamic::*, marshal::*, object_meta::*, resource::*,
+    resource_requirements::*,
 };
 use crate::pervasive_ext::string_view::*;
 use vstd::prelude::*;
@@ -112,6 +113,14 @@ impl FluentBitSpec {
     {
         String::from_rust_string(self.inner.parsers_config.to_string())
     }
+
+    #[verifier(external_body)]
+    pub fn resources(&self) -> (resources: ResourceRequirements)
+        ensures
+            resources@ == self@.resources,
+    {
+        ResourceRequirements::from_kube(self.inner.resources.clone())
+    }
 }
 
 }
diff --git a/src/controller_examples/fluent_controller/exec/reconciler.rs b/src/controller_examples/fluent_controller/exec/reconciler.rs
@@ -450,6 +450,7 @@ fn make_fluentbit_pod_spec(fluentbit: &FluentBit) -> (pod_spec: PodSpec)
                 }
                 ports
             });
+            fluentbit_container.set_resources(fluentbit.spec().resources());
             fluentbit_container
         });
         proof {

diff --git a/src/controller_examples/fluent_controller/spec/fluentbit.rs b/src/controller_examples/fluent_controller/spec/fluentbit.rs
@@ -3,6 +3,7 @@
 use crate::kubernetes_api_objects::error::ParseDynamicObjectError;
 use crate::kubernetes_api_objects::{
     api_resource::*, common::*, dynamic::*, marshal::*, object_meta::*, resource::*,
+    resource_requirements::*,
 };
 use crate::pervasive_ext::string_view::*;
 use vstd::prelude::*;
@@ -89,6 +90,7 @@ impl ResourceView for FluentBitView {
 pub struct FluentBitSpecView {
     pub fluentbit_config: StringView,
     pub parsers_config: StringView,
+    pub resources: ResourceRequirementsView,
 }
 
 impl FluentBitSpecView {}

diff --git a/src/controller_examples/fluent_controller/spec/reconciler.rs b/src/controller_examples/fluent_controller/spec/reconciler.rs
@@ -330,6 +330,7 @@ pub open spec fn make_fluentbit_pod_spec(fluentbit: FluentBitView) -> PodSpecVie
                         .set_name(new_strlit("metrics")@)
                         .set_container_port(2020),
                 ])
+                .set_resources(fluentbit.spec.resources)
         ])
 }
 

diff --git a/src/deps_hack/Cargo.lock b/src/deps_hack/Cargo.lock
diff --git a/src/deps_hack/Cargo.toml b/src/deps_hack/Cargo.toml
@@ -18,7 +18,7 @@ kube = { version = "0.78.0", default-features = false, features = ["admission"]
 kube-derive = { version = "0.78.0", default-features = false } # only needed to opt out of schema
 kube-client = { version = "0.78.0", default-features = false }
 kube-core = { version = "0.78.0", default-features = false }
-k8s-openapi = { version = "0.17.0", default-features = false }
+k8s-openapi = { version = "0.17.0", default-features = false, features = ["schemars"] }
 tokio = { version = "1.14.0", features = ["full"] }
 serde = { version = "1.0.130", features = ["derive"] }
 serde_json = "1.0.68"

diff --git a/src/deps_hack/src/lib.rs b/src/deps_hack/src/lib.rs
@@ -73,4 +73,6 @@ pub struct FluentBitSpec {
     pub fluentbit_config: String,
     #[serde(rename = "parsersConfig")]
     pub parsers_config: String,
+    #[serde(default)]
+    pub resources: k8s_openapi::api::core::v1::ResourceRequirements,
 }
diff --git a/src/kubernetes_api_objects/pod.rs b/src/kubernetes_api_objects/pod.rs
@@ -7,6 +7,7 @@ use crate::kubernetes_api_objects::error::ParseDynamicObjectError;
 use crate::kubernetes_api_objects::marshal::*;
 use crate::kubernetes_api_objects::object_meta::*;
 use crate::kubernetes_api_objects::resource::*;
+use crate::kubernetes_api_objects::resource_requirements::*;
 use crate::pervasive_ext::string_view::*;
 use vstd::prelude::*;
 use vstd::seq_lib::*;
@@ -246,6 +247,14 @@ impl Container {
         self.inner.lifecycle = std::option::Option::Some(lifecycle.into_kube())
     }
 
+    #[verifier(external_body)]
+    pub fn set_resources(&mut self, resources: ResourceRequirements)
+        ensures
+            self@ == old(self)@.set_resources(resources@),
+    {
+        self.inner.resources = std::option::Option::Some(resources.into_kube())
+    }
+
     // Methods for the fields that do not appear in spec
 
     #[verifier(external_body)]
@@ -1181,6 +1190,7 @@ pub struct ContainerView {
     pub ports: Option<Seq<ContainerPortView>>,
     pub volume_mounts: Option<Seq<VolumeMountView>>,
     pub lifecycle: Option<LifecycleView>,
+    pub resources: Option<ResourceRequirementsView>,
 }
 
 impl ContainerView {
@@ -1191,6 +1201,7 @@ impl ContainerView {
             ports: Option::None,
             volume_mounts: Option::None,
             lifecycle: Option::None,
+            resources: Option::None,
         }
     }
 
@@ -1228,6 +1239,13 @@ impl ContainerView {
             ..self
         }
     }
+
+    pub open spec fn set_resources(self, resources: ResourceRequirementsView) -> ContainerView {
+        ContainerView {
+            resources: Option::Some(resources),
+            ..self
+        }
+    }
 }
 
 impl Marshalable for ContainerView {

diff --git a/src/kubernetes_api_objects/resource_requirements.rs b/src/kubernetes_api_objects/resource_requirements.rs
@@ -10,18 +10,26 @@ pub struct ResourceRequirements {
     inner: deps_hack::k8s_openapi::api::core::v1::ResourceRequirements
 }
 
-impl ResourceWrapper<deps_hack::k8s_openapi::api::core::v1::ResourceRequirements> for ResourceRequirements {
+impl ResourceRequirements {
+    pub spec fn view(&self) -> ResourceRequirementsView;
+
     #[verifier(external)]
-    fn from_kube(inner: deps_hack::k8s_openapi::api::core::v1::ResourceRequirements) -> ResourceRequirements {
+    pub fn from_kube(inner: deps_hack::k8s_openapi::api::core::v1::ResourceRequirements) -> ResourceRequirements {
         ResourceRequirements { inner: inner }
     }
 
     #[verifier(external)]
-    fn into_kube(self) -> deps_hack::k8s_openapi::api::core::v1::ResourceRequirements {
+    pub fn into_kube(self) -> deps_hack::k8s_openapi::api::core::v1::ResourceRequirements {
         self.inner
     }
 }
 
-impl ResourceRequirements {}
+pub struct ResourceRequirementsView {}
+
+impl ResourceRequirementsView {
+    pub open spec fn default() -> ResourceRequirementsView {
+        ResourceRequirementsView {}
+    }
+}
 
 }