diff --git a/.github/workflows/package-deletion.yml b/.github/workflows/package-deletion.yml index fc6be4639..5a84081ba 100644 --- a/.github/workflows/package-deletion.yml +++ b/.github/workflows/package-deletion.yml @@ -16,4 +16,4 @@ jobs: env: GH_TOKEN: ${{ secrets.GITHUB_TOKEN }} run: | - gh api --method DELETE -H "Accept: application/vnd.github+json" -H "X-GitHub-Api-Version: 2022-11-28" /orgs/vmware-research/packages/container/verifiable-controllers%2F${{ inputs.image }} + gh api --method DELETE -H "Accept: application/vnd.github+json" -H "X-GitHub-Api-Version: 2022-11-28" /orgs/anvil-verifier/packages/container/verifiable-controllers%2F${{ inputs.image }} diff --git a/README.md b/README.md index ff215f1af..0f9b6a937 100644 --- a/README.md +++ b/README.md @@ -1,5 +1,5 @@ -[![License](https://img.shields.io/badge/License-MIT-green.svg)](https://github.com/vmware-research/verifiable-controllers/blob/main/LICENSE) -[![CI](https://github.com/vmware-research/verifiable-controllers/actions/workflows/ci.yml/badge.svg)](https://github.com/vmware-research/verifiable-controllers/actions/workflows/ci.yml) +[![License](https://img.shields.io/badge/License-MIT-green.svg)](https://github.com/anvil-verifier/anvil/blob/main/LICENSE) +[![CI](https://github.com/anvil-verifier/anvil/actions/workflows/ci.yml/badge.svg)](https://github.com/anvil-verifier/anvil/actions/workflows/ci.yml) # Anvil: Building Formally Verified Kubernetes Controllers @@ -9,7 +9,7 @@ So far, we have built and verified three Kubernetes controllers (for managing Zo For now, the best way to use Anvil is to download the source code and import its components into your controller projects, like what we did for our controller [examples](src/controller_examples/). To use Anvil, you will need to install [Verus](https://github.com/verus-lang/verus) (See the [installation instructions](https://github.com/verus-lang/verus/blob/main/INSTALL.md)). Currently Anvil uses Verus version `0d7b766446cd33521132cff03b6108705e83884f`. -If you want to reproduce the results in the OSDI'24 paper "Anvil: Verifying Liveness of Cluster Management Controllers", please refer to the [osdi24](https://github.com/vmware-research/verifiable-controllers/tree/osdi24) branch. +If you want to reproduce the results in the OSDI'24 paper "Anvil: Verifying Liveness of Cluster Management Controllers", please refer to the [osdi24](https://github.com/anvil-verifier/anvil/tree/osdi24) branch. ## Implementing controllers with Anvil diff --git a/deploy/consumer/deploy_remote.yaml b/deploy/consumer/deploy_remote.yaml index c386bad52..7cf59e7c5 100644 --- a/deploy/consumer/deploy_remote.yaml +++ b/deploy/consumer/deploy_remote.yaml @@ -16,6 +16,6 @@ spec: app.kubernetes.io/name: consumer-controller spec: containers: - - image: ghcr.io/vmware-research/verifiable-controllers/consumer-controller:latest + - image: ghcr.io/anvil-verifier/anvil/consumer-controller:latest name: controller serviceAccountName: consumer-controller diff --git a/deploy/fluent/deploy_remote.yaml b/deploy/fluent/deploy_remote.yaml index dfc751660..31507178b 100644 --- a/deploy/fluent/deploy_remote.yaml +++ b/deploy/fluent/deploy_remote.yaml @@ -16,6 +16,6 @@ spec: app.kubernetes.io/name: fluent-controller spec: containers: - - image: ghcr.io/vmware-research/verifiable-controllers/fluent-controller:latest + - image: ghcr.io/anvil-verifier/anvil/fluent-controller:latest name: controller serviceAccountName: fluent-controller diff --git a/deploy/producer/deploy_remote.yaml b/deploy/producer/deploy_remote.yaml index 016ffbf0a..3f1aa5b6a 100644 --- a/deploy/producer/deploy_remote.yaml +++ b/deploy/producer/deploy_remote.yaml @@ -16,6 +16,6 @@ spec: app.kubernetes.io/name: producer-controller spec: containers: - - image: ghcr.io/vmware-research/verifiable-controllers/producer-controller:latest + - image: ghcr.io/anvil-verifier/anvil/producer-controller:latest name: controller serviceAccountName: producer-controller diff --git a/deploy/rabbitmq/deploy_remote.yaml b/deploy/rabbitmq/deploy_remote.yaml index 31fc5ea70..2ce08d8a7 100644 --- a/deploy/rabbitmq/deploy_remote.yaml +++ b/deploy/rabbitmq/deploy_remote.yaml @@ -16,6 +16,6 @@ spec: app.kubernetes.io/name: rabbitmq-controller spec: containers: - - image: ghcr.io/vmware-research/verifiable-controllers/rabbitmq-controller:latest + - image: ghcr.io/anvil-verifier/anvil/rabbitmq-controller:latest name: controller serviceAccountName: rabbitmq-controller diff --git a/deploy/vreplicaset/deploy_remote.yaml b/deploy/vreplicaset/deploy_remote.yaml index b15698468..33c8efe6e 100644 --- a/deploy/vreplicaset/deploy_remote.yaml +++ b/deploy/vreplicaset/deploy_remote.yaml @@ -16,6 +16,6 @@ spec: app.kubernetes.io/name: vreplicaset-controller spec: containers: - - image: ghcr.io/vmware-research/verifiable-controllers/vreplicaset-controller:latest + - image: ghcr.io/anvil-verifier/anvil/vreplicaset-controller:latest name: controller serviceAccountName: vreplicaset-controller diff --git a/deploy/zookeeper/deploy_remote.yaml b/deploy/zookeeper/deploy_remote.yaml index e0e3023de..a541b5c9a 100644 --- a/deploy/zookeeper/deploy_remote.yaml +++ b/deploy/zookeeper/deploy_remote.yaml @@ -16,6 +16,6 @@ spec: app.kubernetes.io/name: zookeeper-controller spec: containers: - - image: ghcr.io/vmware-research/verifiable-controllers/zookeeper-controller:latest + - image: ghcr.io/anvil-verifier/anvil/zookeeper-controller:latest name: controller serviceAccountName: zookeeper-controller diff --git a/docker/ae/Dockerfile b/docker/ae/Dockerfile index 6c1762497..e7706fd89 100644 --- a/docker/ae/Dockerfile +++ b/docker/ae/Dockerfile @@ -1,4 +1,4 @@ -FROM ghcr.io/vmware-research/verifiable-controllers/verus:latest as builder +FROM ghcr.io/anvil-verifier/anvil/verus:latest as builder WORKDIR /anvil diff --git a/docker/controller/Dockerfile b/docker/controller/Dockerfile index 215a4d52e..07377d8b8 100644 --- a/docker/controller/Dockerfile +++ b/docker/controller/Dockerfile @@ -1,4 +1,4 @@ -FROM ghcr.io/vmware-research/verifiable-controllers/verus:latest as builder +FROM ghcr.io/anvil-verifier/anvil/verus:latest as builder ARG APP WORKDIR /anvil diff --git a/src/controller_examples/zookeeper_controller/exec/reconciler.rs b/src/controller_examples/zookeeper_controller/exec/reconciler.rs index 12eabc632..f810c98e5 100644 --- a/src/controller_examples/zookeeper_controller/exec/reconciler.rs +++ b/src/controller_examples/zookeeper_controller/exec/reconciler.rs @@ -114,7 +114,7 @@ pub fn reconcile_core( // the zookeeper cluster might be unavailable because of losing the quorum. // So the controller needs to correctly prompt membership change before reducing the replica // size of the stateful set, by writing the new replica size into the zookeeper API. - // Details can be found in https://github.com/vmware-research/verifiable-controllers/issues/174. + // Details can be found in https://github.com/anvil-verifier/anvil/issues/174. let state_prime = ZookeeperReconcileState { reconcile_step: ZookeeperReconcileStep::AfterExistsZKNode, ..state