From 223f956eb965c6e1ddf5c7562c682d42482070eb Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Tobi=20L=C3=BCtke?= Date: Sun, 13 Sep 2026 02:05:16 +0000 Subject: [PATCH] fix(store): enforce conditions at delete and multipart commit Extract the storage corrections identified in PR #8. S3 conditional delete drops from two requests to one; compose removes its destination HEAD. GCS invalid update tokens fail locally. Include SDK transport regressions and bounded StoreConditions controls/witnesses. --- crates/walgit-store/src/gcs.rs | 41 ++- crates/walgit-store/src/s3.rs | 427 ++++++++++++++++++++++---- docs/ROUNDTRIPS.md | 16 + docs/spec/README.md | 14 + docs/spec/scratch/StoreConditions.cfg | 4 + docs/spec/scratch/StoreConditions.tla | 51 +++ docs/spec/tlc/cases.tsv | 8 + 7 files changed, 489 insertions(+), 72 deletions(-) create mode 100644 docs/spec/scratch/StoreConditions.cfg create mode 100644 docs/spec/scratch/StoreConditions.tla diff --git a/crates/walgit-store/src/gcs.rs b/crates/walgit-store/src/gcs.rs index fbe4a62..4102dc8 100644 --- a/crates/walgit-store/src/gcs.rs +++ b/crates/walgit-store/src/gcs.rs @@ -603,12 +603,15 @@ impl GcsStore { } async fn put_inner(&self, key: &str, body: PutBody, opts: PutOptions) -> Result { + if let PutMode::Update(version) = &opts.mode { + update_generation(version)?; + } let result = match body { PutBody::Bytes(b) => { let (client, _permit) = self.data_client(key, false).await; let mut builder = client.write_object(self.bucket_resource.clone(), key.to_owned(), b); - builder = apply_put_opts(builder, &opts); + builder = apply_put_opts(builder, &opts)?; Box::pin(builder.send_unbuffered()).await } PutBody::File(path) => { @@ -623,7 +626,7 @@ impl GcsStore { key.to_owned(), Bytes::from(bytes), ); - builder = apply_put_opts(builder, &opts); + builder = apply_put_opts(builder, &opts)?; Box::pin(builder.send_unbuffered()).await } else { let stream = crate::util::file_stream(path, None, FILE_CHUNK_SIZE); @@ -633,7 +636,7 @@ impl GcsStore { let (client, _permit) = self.data_client(key, false).await; let mut builder = client.write_object(self.bucket_resource.clone(), key.to_owned(), source); - builder = apply_put_opts(builder, &opts); + builder = apply_put_opts(builder, &opts)?; Box::pin(builder.send_buffered()).await } } @@ -644,7 +647,7 @@ impl GcsStore { let (client, _permit) = self.data_client(key, false).await; let mut builder = client.write_object(self.bucket_resource.clone(), key.to_owned(), bytes); - builder = apply_put_opts(builder, &opts); + builder = apply_put_opts(builder, &opts)?; Box::pin(builder.send_unbuffered()).await } PutBody::Stream { stream, .. } => { @@ -654,7 +657,7 @@ impl GcsStore { let (client, _permit) = self.data_client(key, false).await; let mut builder = client.write_object(self.bucket_resource.clone(), key.to_owned(), source); - builder = apply_put_opts(builder, &opts); + builder = apply_put_opts(builder, &opts)?; Box::pin(builder.send_buffered()).await } }; @@ -1115,12 +1118,19 @@ impl StreamingSource for StoreStreamSource { } } +/// A conditional update must name an existing generation. Zero means create in +/// GCS, so accepting it here would silently change the operation's contract. +fn update_generation(version: &Version) -> Result { + parse_generation(version).filter(|g| *g > 0).ok_or_else(|| { + StoreError::InvalidArgument("GCS update requires a positive generation token".into()) + }) +} + /// Apply put-mode preconditions and metadata to a `WriteObject` builder. -/// Builder methods consume `self` and return `Self`, so we chain them. fn apply_put_opts( mut builder: google_cloud_storage::builder::storage::WriteObject, opts: &PutOptions, -) -> google_cloud_storage::builder::storage::WriteObject +) -> Result> where S: google_cloud_storage::stub::Storage + 'static, { @@ -1130,9 +1140,7 @@ where builder = builder.set_if_generation_match(0_i64); } PutMode::Update(v) => { - if let Some(generation) = parse_generation(v) { - builder = builder.set_if_generation_match(generation); - } + builder = builder.set_if_generation_match(update_generation(v)?); } } @@ -1144,7 +1152,7 @@ where builder = builder.set_cache_control(IMMUTABLE_CACHE_CONTROL); } - builder + Ok(builder) } // ---- error mapping ---- @@ -1246,6 +1254,17 @@ mod tests { assert_eq!(parse_generation(&v), None); } + #[test] + fn update_conditions_cannot_turn_into_create_or_overwrite() { + for token in ["", "invalid", "0", "-1", "9223372036854775808"] { + assert!(matches!( + update_generation(&Version::new(token)), + Err(StoreError::InvalidArgument(_)) + )); + } + assert_eq!(update_generation(&Version::new("42")).unwrap(), 42); + } + #[test] fn range_to_read_range_basic() { let _r = range_to_read_range(&(10..30)); // [10, 30) → offset=10, limit=20 diff --git a/crates/walgit-store/src/s3.rs b/crates/walgit-store/src/s3.rs index d788cc2..c91789c 100644 --- a/crates/walgit-store/src/s3.rs +++ b/crates/walgit-store/src/s3.rs @@ -21,21 +21,14 @@ //! //! ## Conditional DELETE //! -//! S3 has no native conditional delete. We emulate via HEAD (read `ETag`) + -//! compare + DELETE, documenting the inherent check-then-act race: a -//! concurrent writer could replace the object between HEAD and DELETE. -//! Acceptable for walgit's lease-guarded semantics. +//! Conditional DELETE uses native `If-Match` at the storage linearization point. +//! Never substitute a HEAD followed by an unconditional delete. //! //! ## Multipart upload //! -//! Objects above `cfg.multipart_threshold` use `CreateMultipartUpload` + -//! `UploadPart` + `CompleteMultipartUpload`. `CreateMultipartUpload` does NOT -//! support `If-None-Match`/`If-Match` in the S3 API, so multipart is only -//! used for `PutMode::Overwrite`. For walgit's immutable pack objects -//! (`PutMode::Create`) we use single-shot PUT when the object is large, -//! accepting the (tiny) risk of concurrent create races. CAS-rewritten -//! objects (manifests, leases, bundle lists) are always small → single-shot -//! PUT with conditional headers. +//! Objects above `cfg.multipart_threshold` use staged multipart uploads. +//! Create/update conditions apply at completion, when the destination becomes visible. +//! Providers must honor these conditions; errors never trigger an unconditional retry. //! //! ## rustfs compatibility (tested with rustfs/rustfs:latest) //! @@ -369,11 +362,8 @@ impl ObjectStore for S3Store { async fn put(&self, key: &str, body: PutBody, opts: PutOptions) -> Result { let (s3_body, len) = body_to_s3(body).await?; - // Multipart only for Overwrite (CreateMultipartUpload has no - // conditional header support in the S3 API). Create/Update always - // use single-shot PUT. - let use_multipart = - len > self.multipart_threshold && matches!(opts.mode, PutMode::Overwrite); + // Conditions apply to the final publication, not staging. + let use_multipart = len > self.multipart_threshold; if use_multipart { return self.multipart_put(key, s3_body, len, &opts).await; @@ -425,34 +415,48 @@ impl ObjectStore for S3Store { } async fn delete(&self, key: &str, if_version: Option) -> Result<()> { + let mut request = self.client.delete_object().bucket(&self.bucket).key(key); if let Some(want) = &if_version { - // S3 has no conditional delete: emulate via HEAD + compare + DELETE. - // RACE: a concurrent writer could replace the object between HEAD - // and DELETE. Acceptable for walgit's lease-guarded semantics. - let head = self.head(key).await?; - match head { - None => return Err(StoreError::NotFound { key: key.into() }), - Some(meta) if &meta.version != want => { - return Err(StoreError::PreconditionFailed { - key: key.into(), - current: Some(meta.version), - }); - } - _ => {} - } + request = request.if_match(want.as_str()); } - - let resp = self - .client - .delete_object() - .bucket(&self.bucket) - .key(key) - .send() - .await; + let resp = request.send().await; match resp { Ok(_) => Ok(()), Err(err) => { + if err + .raw_response() + .is_some_and(|r| r.status().as_u16() == 404) + || matches!(err_code(&err), Some("NoSuchKey" | "NotFound")) + { + return if if_version.is_some() { + Err(StoreError::NotFound { key: key.into() }) + } else { + Ok(()) + }; + } + + if err + .raw_response() + .is_some_and(|r| r.status().as_u16() == 412) + || matches!( + err_code(&err), + Some("PreconditionFailed" | "ConditionalRequestConflict") + ) + { + // Compatible services may use 412 for an absent key too. + // Probe only after the atomic delete has already refused. + let current = match self.head(key).await { + Ok(None) => return Err(StoreError::NotFound { key: key.into() }), + Ok(Some(meta)) => Some(meta.version), + Err(_) => None, + }; + return Err(StoreError::PreconditionFailed { + key: key.into(), + current, + }); + } + // S3 DeleteObject is idempotent: deleting a non-existent key // returns Ok, not an error. If we get here, it's a real error. // For unconditional deletes we treat any error as transient. @@ -623,14 +627,6 @@ impl ObjectStore for S3Store { "compose needs at least one source".into(), )); } - if let PutMode::Create = opts.mode - && self.head(dest).await?.is_some() - { - return Err(StoreError::PreconditionFailed { - key: dest.to_owned(), - current: None, - }); - } // Sizes first: the layout of parts depends on them. let mut sizes = Vec::with_capacity(sources.len()); for src in sources { @@ -782,19 +778,33 @@ impl ObjectStore for S3Store { let completed = aws_sdk_s3::types::CompletedMultipartUpload::builder() .set_parts(Some(parts)) .build(); - let resp = match self + let complete = self .client .complete_multipart_upload() .bucket(&self.bucket) .key(dest) .upload_id(&upload_id) - .multipart_upload(completed) - .send() - .await - { + .multipart_upload(completed); + let complete = match &opts.mode { + PutMode::Overwrite => complete, + PutMode::Create => complete.if_none_match("*"), + PutMode::Update(v) => complete.if_match(v.as_str()), + }; + let resp = match complete.send().await { Ok(r) => r, Err(e) => { let _ = self.abort_multipart(dest, &upload_id).await; + if e.raw_response().is_some_and(|r| r.status().as_u16() == 412) + || matches!( + err_code(&e), + Some("PreconditionFailed" | "ConditionalRequestConflict") + ) + { + return Err(StoreError::PreconditionFailed { + key: dest.into(), + current: None, + }); + } return Err(classify_error("s3 complete multipart", &e)); } }; @@ -832,7 +842,7 @@ struct ListState { buffer: std::vec::IntoIter>, } -// ---- multipart upload (Overwrite only) --------------------------------- +// ---- multipart upload --------------------------------- impl S3Store { async fn multipart_put( @@ -843,6 +853,11 @@ impl S3Store { opts: &PutOptions, ) -> Result { use tokio::io::AsyncReadExt; + if self.multipart_part_size == 0 || len.div_ceil(self.multipart_part_size) > 10_000 { + return Err(StoreError::InvalidArgument( + "S3 upload requires 1..10000 nonempty parts".into(), + )); + } let mut create = self .client @@ -854,6 +869,10 @@ impl S3Store { create = create.content_type(ct); } + if opts.immutable { + create = create.cache_control("public, max-age=31536000, immutable"); + } + let upload = create .send() .await @@ -898,8 +917,11 @@ impl S3Store { read_total += n; } - if read_total == 0 { - break; + if read_total != to_read { + let _ = self.abort_multipart(key, &upload_id).await; + return Err(StoreError::InvalidArgument( + "S3 upload shorter than declared length".into(), + )); } buf.truncate(read_total); let actual = read_total as u64; @@ -935,23 +957,54 @@ impl S3Store { part_number += 1; } + // Do not commit an input that grew after the caller captured its length. + let mut extra = [0u8; 1]; + match reader.read(&mut extra).await { + Ok(0) => {} + result => { + let _ = self.abort_multipart(key, &upload_id).await; + return Err(StoreError::InvalidArgument( + if result.is_ok() { + "S3 upload longer than declared length" + } else { + "S3 upload failed while validating final length" + } + .into(), + )); + } + } + let completed = aws_sdk_s3::types::CompletedMultipartUpload::builder() .set_parts(Some(uploaded_parts)) .build(); - let resp = match self + let complete = self .client .complete_multipart_upload() .bucket(&self.bucket) .key(key) .upload_id(&upload_id) - .multipart_upload(completed) - .send() - .await - { + .multipart_upload(completed); + let complete = match &opts.mode { + PutMode::Overwrite => complete, + PutMode::Create => complete.if_none_match("*"), + PutMode::Update(v) => complete.if_match(v.as_str()), + }; + let resp = match complete.send().await { Ok(r) => r, Err(e) => { let _ = self.abort_multipart(key, &upload_id).await; + if e.raw_response().is_some_and(|r| r.status().as_u16() == 412) + || matches!( + err_code(&e), + Some("PreconditionFailed" | "ConditionalRequestConflict") + ) + { + return Err(StoreError::PreconditionFailed { + key: key.into(), + current: None, + }); + } return Err(classify_error("s3 complete multipart", &e)); } }; @@ -995,7 +1048,7 @@ fn static_credentials( // 5. ListObjectsV2: StartAfter, ContinuationToken, IsTruncated/NextToken OK. // 6. DeleteObject: idempotent for absent keys (204). // 7. Multipart: CreateMultipartUpload + UploadPart + CompleteMultipartUpload -// supported. No conditional headers on Create/Complete (same as real S3). +// conditions must be honored at CompleteMultipartUpload. // 8. ETags: quoted, MD5 for single-PUT, compound for multipart. Quotes // stripped consistently in our Version. // 9. force_path_style: required for rustfs local dev. @@ -1008,6 +1061,258 @@ mod tests { use aws_sdk_s3::operation::list_objects_v2::ListObjectsV2Error; use aws_sdk_s3::operation::put_object::PutObjectError; + #[derive(Default)] + struct ConditionService { + requests: Vec<(String, String, Option, Option)>, + current: Option, + } + + // Models the storage linearization point, including a rival that already + // replaced the caller's captured version. Actual SDK requests hit this server. + async fn condition_request( + axum::extract::State(state): axum::extract::State< + std::sync::Arc>, + >, + request: axum::extract::Request, + ) -> axum::response::Response { + use axum::response::IntoResponse; + let method = request.method().to_string(); + let query = request.uri().query().unwrap_or("").to_owned(); + let matched = request + .headers() + .get("if-match") + .map(|h| h.to_str().unwrap().to_owned()); + let absent = request + .headers() + .get("if-none-match") + .map(|h| h.to_str().unwrap().to_owned()); + // Drain the staged body before replying, as a real HTTP server would. + axum::body::to_bytes(request.into_body(), 1024) + .await + .unwrap(); + let mut state = state.lock(); + state.requests.push(( + method.clone(), + query.clone(), + matched.clone(), + absent.clone(), + )); + if method == "HEAD" { + if state.current.is_none() { + return axum::http::StatusCode::NOT_FOUND.into_response(); + } + // A HEAD-before-DELETE implementation sees its old token; the rival + // is already current when the subsequent delete is evaluated. + return ( + [("etag", "\"captured\""), ("content-length", "5242880")], + "", + ) + .into_response(); + } + if method == "POST" && query.starts_with("uploads") { + return "attempt".into_response(); + } + if method == "PUT" { + return ( + [("etag", "\"part\"")], + "\"part\"", + ) + .into_response(); + } + if method == "DELETE" && query.contains("uploadId") { + return axum::http::StatusCode::NO_CONTENT.into_response(); + } + if method == "DELETE" && matched.is_some() && state.current.is_none() { + return ( + axum::http::StatusCode::PRECONDITION_FAILED, + "PreconditionFailed", + ) + .into_response(); + } + if matched + .as_ref() + .is_some_and(|v| Some(v) != state.current.as_ref()) + || (absent.as_deref() == Some("*") && state.current.is_some()) + { + return ( + axum::http::StatusCode::PRECONDITION_FAILED, + "PreconditionFailed", + ) + .into_response(); + } + if method == "DELETE" { + state.current = None; + axum::http::StatusCode::NO_CONTENT.into_response() + } else { + state.current = Some("published".into()); + "\"published\"".into_response() + } + } + + async fn condition_store() -> ( + S3Store, + std::sync::Arc>, + tokio::task::JoinHandle<()>, + ) { + let state = std::sync::Arc::new(parking_lot::Mutex::new(ConditionService { + current: Some("rival".into()), + ..Default::default() + })); + let app = axum::Router::new() + .fallback(condition_request) + .with_state(state.clone()); + let listener = tokio::net::TcpListener::bind("127.0.0.1:0").await.unwrap(); + let endpoint = format!("http://{}", listener.local_addr().unwrap()); + let task = tokio::spawn(async move { axum::serve(listener, app).await.unwrap() }); + let config = aws_sdk_s3::Config::builder() + .region(aws_sdk_s3::config::Region::new("us-east-1")) + .credentials_provider(Credentials::new( + "synthetic", + "synthetic", + None, + None, + "test", + )) + .endpoint_url(endpoint) + .force_path_style(true) + .behavior_version_latest() + .retry_config(aws_sdk_s3::config::retry::RetryConfig::disabled()) + .build(); + ( + S3Store { + client: S3Client::from_conf(config), + bucket: "bucket".into(), + http: reqwest::Client::new(), + multipart_threshold: 1, + multipart_part_size: 8, + }, + state, + task, + ) + } + + #[tokio::test] + async fn conditional_delete_preserves_rivals_and_only_probes_on_failure() { + let (store, state, server) = condition_store().await; + assert!(matches!( + store.delete("key", Some(Version::new("captured"))).await, + Err(StoreError::PreconditionFailed { .. }) + )); + { + let state = state.lock(); + assert_eq!(state.current.as_deref(), Some("rival")); + assert_eq!(state.requests.len(), 2); + assert_eq!(state.requests[0].0, "DELETE", "no HEAD/check/delete window"); + assert_eq!(state.requests[1].0, "HEAD", "failure-only probe"); + assert_eq!(state.requests[0].2.as_deref(), Some("captured")); + } + store + .delete("key", Some(Version::new("rival"))) + .await + .unwrap(); + assert!(state.lock().current.is_none()); + assert_eq!( + state.lock().requests.len(), + 3, + "successful delete uses one request" + ); + assert!(matches!( + store.delete("key", Some(Version::new("rival"))).await, + Err(StoreError::NotFound { .. }) + )); + server.abort(); + } + + #[tokio::test] + async fn staged_put_and_compose_conditions_hold_at_completion() { + for compose in [false, true] { + for mode in [ + PutMode::Create, + PutMode::Update(Version::new("captured")), + PutMode::Update(Version::new("rival")), + ] { + let (store, state, server) = condition_store().await; + let opts = PutOptions { + mode: mode.clone(), + ..Default::default() + }; + let result = if compose { + // One source is copied server-side before conditional completion. + store.compose("dest", &["source".into()], opts).await + } else { + store + .put("dest", PutBody::Bytes(Bytes::from_static(b"sample")), opts) + .await + }; + let success = matches!(&mode, PutMode::Update(v) if v.as_str() == "rival"); + if success { + assert!(result.is_ok(), "{result:?}"); + } else { + assert!( + matches!(result, Err(StoreError::PreconditionFailed { .. })), + "{result:?}" + ); + } + let state = state.lock(); + assert_eq!( + state.current.as_deref(), + Some(if success { "published" } else { "rival" }) + ); + let completes: Vec<_> = state + .requests + .iter() + .filter(|(m, q, _, _)| m == "POST" && q.contains("uploadId")) + .collect(); + assert_eq!(completes.len(), 1); + assert_eq!( + completes[0].3.as_deref(), + matches!(mode, PutMode::Create).then_some("*") + ); + assert_eq!( + state + .requests + .iter() + .filter(|(m, q, _, _)| m == "DELETE" && q.contains("uploadId")) + .count(), + usize::from(!success) + ); + server.abort(); + } + } + } + + #[tokio::test] + async fn multipart_length_mismatch_never_reaches_completion() { + for declared in [3, 12] { + let (store, state, server) = condition_store().await; + let result = store + .multipart_put( + "key", + S3ByteStream::from_static(b"sample"), + declared, + &PutOptions { + mode: PutMode::Update(Version::new("rival")), + ..Default::default() + }, + ) + .await; + assert!( + matches!(result, Err(StoreError::InvalidArgument(_))), + "{result:?}" + ); + let state = state.lock(); + assert_eq!(state.current.as_deref(), Some("rival")); + assert!( + !state + .requests + .iter() + .any(|(method, query, _, _)| method == "POST" && query.contains("uploadId")) + ); + assert_eq!(state.requests.iter().filter(|(method, query, _, _)| method == "DELETE" && query.contains("uploadId")).count(), 1); + server.abort(); + } + } + /// A fake S3 that answers every request with one status and error code. /// Bound on an ephemeral port; the accept loop dies with the test runtime. async fn fake_s3(status: u16, code: &'static str) -> S3Client { diff --git a/docs/ROUNDTRIPS.md b/docs/ROUNDTRIPS.md index 447af90..08eef6e 100644 --- a/docs/ROUNDTRIPS.md +++ b/docs/ROUNDTRIPS.md @@ -109,3 +109,19 @@ link, so a scenario can assert "a push on a healthy link is ≤ N requests" as a - What moved to the failure path, and how often that path runs (measured or reasoned). - Which CAS'd object's write rate changes. - Sim scenario(s) covering the new failure mode; `Stats::ops` budget assertion if the hot path changed. + +### Conditional storage operations (2026-09-13) + +S3 conditional DELETE is one conditional DELETE (formerly HEAD → unconditional DELETE, +2 requests/depth). A 412 may add one failure-only HEAD to distinguish an absent key on compatible services; successful deletes never probe. +S3 compose removes its destination existence HEAD; source HEADs/staging are unchanged and +create/update preconditions apply at the final multipart commit. Large conditional PUTs +now use bounded multipart staging plus conditional completion instead of a single PUT. +There is no unconditional retry when a provider refuses the conditional operation. +GCS invalid update tokens fail locally with zero requests, rather than dropping the +condition. These preserve C3/C7/B5 at the actual storage commit point. + +AWS documents the native conditions for [DELETE](https://docs.aws.amazon.com/AmazonS3/latest/API/API_DeleteObject.html) +and [multipart completion](https://docs.aws.amazon.com/AmazonS3/latest/API/API_CompleteMultipartUpload.html). +The SDK-transport tests assert headers, stale-token rejection, surviving rival data and +multipart aborts. Model/negative controls and witnesses: `StoreConditions`. diff --git a/docs/spec/README.md b/docs/spec/README.md index c3adef7..78cdb0c 100644 --- a/docs/spec/README.md +++ b/docs/spec/README.md @@ -120,3 +120,17 @@ The [source range](https://github.com/tlaplus/tlaplus/compare/b123b22...867aefb) changes and empty-set equality, enumeration and fingerprint corrections; it is not a semantics-neutral update. Historical state counts are not reused as new evidence. The runner does not substitute another checker, especially one without equivalent result, liveness and input semantics. + +### Conditional backend operations + +C3/C7/B5 → S3 native conditional delete and multipart completion; GCS rejects invalid, +zero and negative update generations instead of silently changing the operation. +`StoreConditions` checks the mutation point with separate capture, probe/staging, rival +write and commit actions. Its delete-window, staging-window and invalid-token mutations +must each violate `MutationCondition`; separate witnesses reach rejected rivals and +successful delete/create/update. Rust twins are +`conditional_delete_preserves_rivals_and_only_probes_on_failure`, +`staged_put_and_compose_conditions_hold_at_completion`, and +`update_conditions_cannot_turn_into_create_or_overwrite`. +The model uses distinct versions; content-token ABA remains in `LogSlotClaim`. +It does not certify a compatible service's implementation of conditional headers. diff --git a/docs/spec/scratch/StoreConditions.cfg b/docs/spec/scratch/StoreConditions.cfg new file mode 100644 index 0000000..84bae67 --- /dev/null +++ b/docs/spec/scratch/StoreConditions.cfg @@ -0,0 +1,4 @@ +SPECIFICATION Spec +CONSTANTS + Fault = "none" +INVARIANTS TypeOK MutationCondition RivalSurvives diff --git a/docs/spec/scratch/StoreConditions.tla b/docs/spec/scratch/StoreConditions.tla new file mode 100644 index 0000000..b28f5e4 --- /dev/null +++ b/docs/spec/scratch/StoreConditions.tla @@ -0,0 +1,51 @@ +------------------------- MODULE StoreConditions ------------------------- +(* Conditional storage must check the token at the mutation, not at an earlier + HEAD or staging step. Versions here are distinct; content-token ABA is modeled + separately by LogSlotClaim. No network/auth/pack-byte refinement is claimed. *) +EXTENDS Naturals, TLC +CONSTANT Fault +VARIABLES op, bucket, pc, token, probe, raced, accepted, basis +vars == <> +Ops == {"delete", "create", "update", "invalid"} +Init == + /\ op \in Ops + /\ bucket = IF op = "create" THEN "absent" ELSE "old" + /\ pc = "capture" /\ token = "none" /\ probe = FALSE + /\ raced = FALSE /\ accepted = FALSE /\ basis = "none" +Capture == + /\ pc = "capture" + /\ token' = IF op = "invalid" THEN "invalid" ELSE bucket + /\ pc' = "probe" + /\ UNCHANGED <> +Probe == + /\ pc = "probe" + /\ probe' = (bucket = token) + /\ pc' = "commit" + /\ UNCHANGED <> +Rival == + /\ pc \in {"probe", "commit"} /\ ~raced + /\ bucket' = "rival" /\ raced' = TRUE + /\ UNCHANGED <> +Allowed == + IF Fault = "invalid" /\ op = "invalid" THEN TRUE + ELSE IF Fault = "delete" /\ op = "delete" THEN probe + ELSE IF Fault = "staging" /\ op \in {"create", "update"} THEN probe + ELSE op # "invalid" /\ bucket = token +Commit == + /\ pc = "commit" + /\ accepted' = Allowed /\ basis' = bucket + /\ bucket' = IF Allowed THEN (IF op = "delete" THEN "absent" ELSE "published") ELSE bucket + /\ pc' = "done" + /\ UNCHANGED <> +Next == Capture \/ Probe \/ Rival \/ Commit \/ UNCHANGED vars +Spec == Init /\ [][Next]_vars +TypeOK == /\ op \in Ops /\ pc \in {"capture", "probe", "commit", "done"} + /\ bucket \in {"absent", "old", "rival", "published"} + /\ probe \in BOOLEAN /\ raced \in BOOLEAN /\ accepted \in BOOLEAN +MutationCondition == accepted => (op # "invalid" /\ basis = token) +RivalSurvives == (pc = "done" /\ raced) => (~accepted /\ bucket = "rival") +NoRejectedRace == ~(pc = "done" /\ raced /\ ~accepted /\ op # "invalid") +NoSuccessfulDelete == ~(pc = "done" /\ op = "delete" /\ accepted) +NoSuccessfulCreate == ~(pc = "done" /\ op = "create" /\ accepted) +NoSuccessfulUpdate == ~(pc = "done" /\ op = "update" /\ accepted) +============================================================================= diff --git a/docs/spec/tlc/cases.tsv b/docs/spec/tlc/cases.tsv index 4b2f9a9..a64849c 100644 --- a/docs/spec/tlc/cases.tsv +++ b/docs/spec/tlc/cases.tsv @@ -165,3 +165,11 @@ witness-temp-cancel-recovery TempReclaim TempReclaim_w_cancel - - - NoCancelReco witness-temp-full-occupancy TempReclaim TempReclaim_w_full - - - NoFullOccupancy witness-temp-lane-reclaim TempReclaim TempReclaim_w_lane - - - NoLaneReclaim witness-temp-sweep-past-peer TempReclaim TempReclaim_w_peer - - - NoSweepPastPeer +store-conditions StoreConditions StoreConditions - none - pass +bug-store-delete-window StoreConditions StoreConditions - delete - MutationCondition +bug-store-staging-window StoreConditions StoreConditions - staging - MutationCondition +bug-store-invalid-token StoreConditions StoreConditions - invalid - MutationCondition +witness-store-rival-rejection StoreConditions StoreConditions - none - NoRejectedRace +witness-store-delete StoreConditions StoreConditions - none - NoSuccessfulDelete +witness-store-create StoreConditions StoreConditions - none - NoSuccessfulCreate +witness-store-update StoreConditions StoreConditions - none - NoSuccessfulUpdate