Skip to content

Commit

Permalink
Fix links pointing to the old repo (anvil-verifier#567)
Browse files Browse the repository at this point in the history
Signed-off-by: Xudong Sun <[email protected]>
  • Loading branch information
marshtompsxd authored Oct 16, 2024
1 parent 3cc30cf commit 0138e00
Show file tree
Hide file tree
Showing 11 changed files with 13 additions and 13 deletions.
2 changes: 1 addition & 1 deletion .github/workflows/package-deletion.yml
Original file line number Diff line number Diff line change
Expand Up @@ -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 }}
6 changes: 3 additions & 3 deletions README.md
Original file line number Diff line number Diff line change
@@ -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

Expand All @@ -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

Expand Down
2 changes: 1 addition & 1 deletion deploy/consumer/deploy_remote.yaml
Original file line number Diff line number Diff line change
Expand Up @@ -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
2 changes: 1 addition & 1 deletion deploy/fluent/deploy_remote.yaml
Original file line number Diff line number Diff line change
Expand Up @@ -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
2 changes: 1 addition & 1 deletion deploy/producer/deploy_remote.yaml
Original file line number Diff line number Diff line change
Expand Up @@ -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
2 changes: 1 addition & 1 deletion deploy/rabbitmq/deploy_remote.yaml
Original file line number Diff line number Diff line change
Expand Up @@ -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
2 changes: 1 addition & 1 deletion deploy/vreplicaset/deploy_remote.yaml
Original file line number Diff line number Diff line change
Expand Up @@ -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
2 changes: 1 addition & 1 deletion deploy/zookeeper/deploy_remote.yaml
Original file line number Diff line number Diff line change
Expand Up @@ -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
2 changes: 1 addition & 1 deletion docker/ae/Dockerfile
Original file line number Diff line number Diff line change
@@ -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

Expand Down
2 changes: 1 addition & 1 deletion docker/controller/Dockerfile
Original file line number Diff line number Diff line change
@@ -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
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down

0 comments on commit 0138e00

Please sign in to comment.