Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Fix links pointing to the old repo #567

Merged
merged 1 commit into from
Oct 16, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
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
Loading