Support generate_name in the API server model
#499
Merged
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Signed-off-by: Xudong Sun <[email protected]>
Signed-off-by: Xudong Sun <[email protected]>
Signed-off-by: Xudong Sun <[email protected]>
Signed-off-by: Xudong Sun <[email protected]>
Signed-off-by: Xudong Sun <[email protected]>
…ight Signed-off-by: Xudong Sun <[email protected]>
Signed-off-by: Xudong Sun <[email protected]>
Signed-off-by: Xudong Sun <[email protected]>
Signed-off-by: Xudong Sun <[email protected]>
Signed-off-by: Xudong Sun <[email protected]>
Signed-off-by: Xudong Sun <[email protected]>
Signed-off-by: Xudong Sun <[email protected]>
marshtompsxd
changed the title
generate_name in the API server model
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This PR revises the API server model to allow resource creation requests that carry a
generate_namerather than aname. For such requests, the API server will generate a unique name for the object and create the object with the generated name. Before the revision, such requests are rejected by our model. We do not specify the details on how the API server guarantees the uniqueness of the generated name, but rather use a trusted proof function saying that the generated name is different from any existing names. Note that this trusted proof is better written as a "spec ensures" once that gets supported by Verus.We make this revision mainly to enable verifying Kubernetes core controllers such as the ReplicaSet controller that often creates pods with
generate_name.This revision breaks many proofs of the custom controllers we have built, but it is straightforward to fix these broken proofs. In most cases, we only need to say that there does not exist any create request that might create the "same" object.