#!/usr/bin/env bash set -euo pipefail ROOT="$(cd "$(dirname "$0")/../.." && pwd)" source "$ROOT/tests/kind/lib.sh" USER_KUBECONFIG_BEFORE="$(user_kubeconfig_digest)" SUCCEEDED=false OWNS_FIXTURE=false APP_IMAGE=nuthatch-wp10:local cleanup() { local status=$? trap - EXIT INT TERM if [[ "${NUTHATCH_TESTBED_RETAIN:-0}" = 1 ]] && [[ "$SUCCEEDED" != true ]]; then printf 'retained kubeconfig: %s\n' "$KUBECONFIG_PATH" printf 'retained context: %s\n' "$CONTEXT" exit "$status" fi if [[ "$OWNS_FIXTURE" = true ]]; then destroy_fixture || status=1 fi if [[ "$(user_kubeconfig_digest)" != "$USER_KUBECONFIG_BEFORE" ]]; then printf 'user kubeconfig changed unexpectedly\n' >&2 status=1 fi exit "$status" } trap cleanup EXIT trap 'exit 130' INT trap 'exit 143' TERM set_target_available() { local target="$1" local selector="$target" if [[ "$2" = false ]]; then selector=wp10-unavailable fi kube --namespace "$FIXTURE_NAMESPACE" patch service "$target" \ --type merge \ --patch "{\"spec\":{\"selector\":{\"app\":\"$selector\"}}}" >/dev/null } set_postgres_available() { local selector=postgres if [[ "$1" = false ]]; then selector=wp10-unavailable fi kube --namespace "$FIXTURE_NAMESPACE" patch service postgres \ --type merge \ --patch "{\"spec\":{\"selector\":{\"app\":\"$selector\"}}}" >/dev/null } database_connection_count() { local database="$1" kube --namespace "$FIXTURE_NAMESPACE" exec deployment/postgres -- \ env PGPASSWORD=synthetic-postgres psql \ --username nuthatch \ --dbname postgres \ --tuples-only \ --no-align \ --set ON_ERROR_STOP=1 \ --command \ "SELECT count(*) FROM pg_stat_activity WHERE datname = '$database' AND pid <> pg_backend_pid()" | tr -d '[:space:]' } terminate_database_connections() { local database="$1" kube --namespace "$FIXTURE_NAMESPACE" exec deployment/postgres -- \ env PGPASSWORD=synthetic-postgres psql \ --username nuthatch \ --dbname postgres \ --set ON_ERROR_STOP=1 \ --command \ "SELECT pg_terminate_backend(pid) FROM pg_stat_activity WHERE datname = '$database' AND pid <> pg_backend_pid()" \ >/dev/null } render_mode() { local lane="$1" local profile="$2" local mode="$3" local job="wp10-$mode-$lane" render_lane_job \ "$job" \ "$TESTBED/wp10-job.yaml.in" \ "$APP_IMAGE" \ "$profile" sed -i "s|@@MODE@@|$mode|g" "$RUNTIME/$job.yaml" } run_mode() { local lane="$1" local profile="$2" local mode="$3" local job="wp10-$mode-$lane" render_mode "$lane" "$profile" "$mode" run_job_manifest "$job" "$RUNTIME/$job.yaml" } start_mode() { local lane="$1" local profile="$2" local mode="$3" local job="wp10-$mode-$lane" render_mode "$lane" "$profile" "$mode" kube apply --filename "$RUNTIME/$job.yaml" >/dev/null } wait_for_mode_log() { local lane="$1" local mode="$2" local message="$3" local job="wp10-$mode-$lane" for _ in $(seq 1 120); do if kube --namespace "$FIXTURE_NAMESPACE" logs "job/$job" 2>/dev/null | grep -F "$message" >/dev/null; then return fi sleep 0.25 done printf 'timed out waiting for %s\n' "$message" >&2 return 1 } stop_mode() { local lane="$1" local mode="$2" kube --namespace "$FIXTURE_NAMESPACE" delete "job/wp10-$mode-$lane" \ --ignore-not-found >/dev/null } verify_mapping() { local lane="$1" local log="$RUNTIME/wp10-full-$lane.log" kube --namespace "$FIXTURE_NAMESPACE" logs "job/wp10-full-$lane" >"$log" local actions=( FirstRequest ReplayRequest ConflictRequest PrepareEffect DispatchEffect LoseUploadBody SettleLostUpload ExternalEffectApplied ExternalEffectNotApplied FinalizeSuccess FinalizeFailure ControllerAdvance StoreSettlement ) local invariants=( TypeOK RecordIdentityConsistent PersonalRequestsUseOwnPool PersonalPoolsDisjoint FingerprintBindsRequest ReservationsConsistent LocksConsistent ActiveObjectConsistent ExternalStateConsistent UploadBodyConsistent QuotaReservationBound ObjectStateCovered ObjectQuotaBound AccountingAtQuiescence ObservationConsistent RecordsNeverForgotten RequestBindingsStable TerminalRecordsStable SettledEffectsDoNotMutate UnfinishedEventuallyTerminal LostUploadEventuallyTerminal ) local name for name in "${actions[@]}"; do grep -F "protocol action covered: $name" "$log" >/dev/null rg -q "^$name(\\(| ==)" "$ROOT/docs/protocol/Nuthatch.tla" done for name in "${invariants[@]}"; do grep -F "protocol invariant checked: $name" "$log" >/dev/null rg -q "^$name(\\(| ==)" "$ROOT/docs/protocol/Nuthatch.tla" done } acquire_fixture_lock OWNS_FIXTURE=true setup_fixture durable coordination target "$NUTHATCH_REAL_NERDCTL" --namespace "$NERDCTL_NAMESPACE" build \ --file "$ROOT/Dockerfile" \ --target test-runtime \ --tag "$APP_IMAGE" \ "$ROOT" load_local_image "$APP_IMAGE" "$NERDCTL_NAMESPACE" while IFS=$'\t' read -r lane coordination oidc target; do if [[ -n "${NUTHATCH_WP10_TARGET:-}" ]] && [[ "$target" != "$NUTHATCH_WP10_TARGET" ]]; then continue fi profile="$(write_lane_profile "$lane" redis - "$target")" printf 'Running WP10 lane %s: target=%s\n' "$lane" "$target" run_mode "$lane" "$profile" full verify_mapping "$lane" start_mode "$lane" "$profile" pg-prepare wait_for_mode_log "$lane" pg-prepare "PostgreSQL transition fixture ready" printf 'Checking PostgreSQL loss and restoration for %s\n' "$target" set_postgres_available false active_connections="$(database_connection_count "nuthatch_lane_$lane")" test "$active_connections" -gt 0 terminate_database_connections "nuthatch_lane_$lane" || true remaining_connections="$(database_connection_count "nuthatch_lane_$lane")" test "$remaining_connections" = 0 stop_mode "$lane" pg-prepare run_mode "$lane" "$profile" pg-fence set_postgres_available true run_mode "$lane" "$profile" pg-restored kube --namespace "$FIXTURE_NAMESPACE" logs "job/wp10-pg-fence-$lane" | grep -F "protocol action covered: LosePostgres" >/dev/null kube --namespace "$FIXTURE_NAMESPACE" logs "job/wp10-pg-restored-$lane" | grep -F "protocol action covered: RestorePostgres" >/dev/null kube --namespace "$FIXTURE_NAMESPACE" logs "job/wp10-pg-restored-$lane" | grep -F "protocol invariant checked: PostgresFailureFencesDurableState" \ >/dev/null rg -q '^LosePostgres(\(| ==)' "$ROOT/docs/protocol/Nuthatch.tla" rg -q '^RestorePostgres(\(| ==)' "$ROOT/docs/protocol/Nuthatch.tla" rg -q '^PostgresFailureFencesDurableState(\(| ==)' \ "$ROOT/docs/protocol/Nuthatch.tla" run_mode "$lane" "$profile" store-prepare printf 'Checking store-down admission fence for %s\n' "$target" set_target_available "$target" false run_mode "$lane" "$profile" fence printf 'Checking restored store observation for %s\n' "$target" set_target_available "$target" true run_mode "$lane" "$profile" restored kube --namespace "$FIXTURE_NAMESPACE" logs "job/wp10-fence-$lane" | grep -F "store-down rejection creates no protocol record" >/dev/null kube --namespace "$FIXTURE_NAMESPACE" logs "job/wp10-restored-$lane" | grep -F "protocol action covered: RestoreObjectStore" >/dev/null kube --namespace "$FIXTURE_NAMESPACE" logs "job/wp10-restored-$lane" | grep -F "protocol invariant checked: ObjectStoreFailureFencesObjects" >/dev/null rg -q '^LoseObjectStore(\(| ==)' "$ROOT/docs/protocol/Nuthatch.tla" rg -q '^RestoreObjectStore(\(| ==)' "$ROOT/docs/protocol/Nuthatch.tla" rg -q '^ObjectStoreFailureFencesObjects(\(| ==)' \ "$ROOT/docs/protocol/Nuthatch.tla" cleanup_lane_state "$lane" redis - "$target" cleanup_lane_resources "wp10-full-$lane" "$profile" cleanup_lane_resources "wp10-pg-prepare-$lane" "$profile" cleanup_lane_resources "wp10-pg-fence-$lane" "$profile" cleanup_lane_resources "wp10-pg-restored-$lane" "$profile" cleanup_lane_resources "wp10-store-prepare-$lane" "$profile" cleanup_lane_resources "wp10-fence-$lane" "$profile" cleanup_lane_resources "wp10-restored-$lane" "$profile" rm -f "$RUNTIME/wp10-full-$lane.log" done < <(expand_fixture_matrix target) SUCCEEDED=true printf 'Nuthatch WP-10 protocol gate passed\n'