From 2c575ee476e933ec40c9a090ffdd67544574e9dc Mon Sep 17 00:00:00 2001 From: Li-yao Xia Date: Thu, 12 Mar 2026 09:41:51 +0100 Subject: [PATCH 1/6] Adapt to atomic_sc changes --- src/ex3_parallel_add.rs | 5 ++--- src/solutions/ex3_parallel_add.rs | 11 +++++------ 2 files changed, 7 insertions(+), 9 deletions(-) diff --git a/src/ex3_parallel_add.rs b/src/ex3_parallel_add.rs index 6ce8dfd..620d3b5 100644 --- a/src/ex3_parallel_add.rs +++ b/src/ex3_parallel_add.rs @@ -6,7 +6,6 @@ #[allow(unused)] // TODO: Remove this use creusot_std::{ ghost::{ - Committer, invariant::{AtomicInvariant, Protocol, Tokens, declare_namespace}, perm::Perm, resource::{Authority, Fragment}, @@ -16,8 +15,8 @@ use creusot_std::{ }; use std::sync::atomic::AtomicI32; -// TODO: Replace with the creusot_std version of AtomicI32 -// use creusot_std::std::sync::AtomicI32; +// TODO: Replace with the creusot_std version of AtomicI32 (you will also need the committer ☺) +// use creusot_std::std::sync::{AtomicI32, UpdateCommitter}; use std::thread; // TODO: Replace with the creusot_std version of thread diff --git a/src/solutions/ex3_parallel_add.rs b/src/solutions/ex3_parallel_add.rs index 411da29..d5f07f3 100644 --- a/src/solutions/ex3_parallel_add.rs +++ b/src/solutions/ex3_parallel_add.rs @@ -1,8 +1,7 @@ -use creusot_std::std::sync::atomic_sc::AtomicI32; +use creusot_std::std::sync::atomic_sc::{AtomicI32, UpdateCommitter}; use creusot_std::{ ghost::{ - Committer, - invariant::{AtomicInvariant, Protocol, Tokens, declare_namespace}, + invariant::{AtomicInvariantSC, Protocol, Tokens, declare_namespace}, perm::Perm, resource::{Authority, Fragment}, }, @@ -48,7 +47,7 @@ pub fn parallel_add() -> i32 { }; // Initialize our invariant - let inv = AtomicInvariant::new( + let inv = AtomicInvariantSC::new( ghost!(ParallelAddAtomicInv { own: own.into_inner(), auth1: auth1.into_inner(), @@ -70,7 +69,7 @@ pub fn parallel_add() -> i32 { let t1 = s.spawn(move |tokens: Ghost| { atomic.fetch_add( 2, - ghost! { |c: &mut Committer| { + ghost! { |c: &mut UpdateCommitter| { inv.open(tokens.into_inner(), |inv: &mut ParallelAddAtomicInv| { inv.auth1.update(*frag1, snapshot!((Some(Excl(true)), Some(Excl(true))))); c.shoot(&mut inv.own); @@ -82,7 +81,7 @@ pub fn parallel_add() -> i32 { let t2 = s.spawn(move |tokens: Ghost| { atomic.fetch_add( 2, - ghost! { |c: &mut Committer| { + ghost! { |c: &mut UpdateCommitter| { inv.open(tokens.into_inner(), |inv: &mut ParallelAddAtomicInv| { inv.auth2.update(*frag2, snapshot!((Some(Excl(true)), Some(Excl(true))))); c.shoot(&mut inv.own); From 2730d0938ce3d3163dcb55130e5d98e42d9d2ddc Mon Sep 17 00:00:00 2001 From: Li-yao Xia Date: Fri, 13 Mar 2026 07:26:48 +0100 Subject: [PATCH 2/6] Bump Creusot version to 0.11.0-dev --- Cargo.lock | 8 ++------ Cargo.toml | 2 +- 2 files changed, 3 insertions(+), 7 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index deb2909..3ae4605 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -10,9 +10,7 @@ checksum = "c08606f8c3cbf4ce6ec8e28fb0014a2c086708fe954eaa885384a6165172e7e8" [[package]] name = "creusot-std" -version = "0.10.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "6496cade7c540734f2db0e40c7a0be29c2fe3a056efdc67b3b7770b56baca4ff" +version = "0.11.0-dev" dependencies = [ "creusot-std-proc", "num-rational", @@ -20,9 +18,7 @@ dependencies = [ [[package]] name = "creusot-std-proc" -version = "0.10.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "a617b331f778b6e199b66057395f63b9d977573e4ca0856a33b8d169d0f0a640" +version = "0.11.0-dev" dependencies = [ "proc-macro2", "quote", diff --git a/Cargo.toml b/Cargo.toml index ac0c90d..b6d02df 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -4,7 +4,7 @@ version = "0.1.0" edition = "2024" [dependencies] -creusot-std = { version = "0.10.0", features = ["sc-drf"] } +creusot-std = { version = "0.11.0-dev", features = ["sc-drf"] } [features] solutions = [] From e17f5accb6762e1e522cc731847a9efda6388986 Mon Sep 17 00:00:00 2001 From: Li-yao Xia Date: Wed, 1 Apr 2026 11:14:44 +0200 Subject: [PATCH 3/6] Adapt to sync changes --- src/ex3_parallel_add.rs | 2 +- src/solutions/ex3_parallel_add.rs | 16 +++++++++------- 2 files changed, 10 insertions(+), 8 deletions(-) diff --git a/src/ex3_parallel_add.rs b/src/ex3_parallel_add.rs index 620d3b5..09d0b68 100644 --- a/src/ex3_parallel_add.rs +++ b/src/ex3_parallel_add.rs @@ -16,7 +16,7 @@ use creusot_std::{ use std::sync::atomic::AtomicI32; // TODO: Replace with the creusot_std version of AtomicI32 (you will also need the committer ☺) -// use creusot_std::std::sync::{AtomicI32, UpdateCommitter}; +// use creusot_std::sync::{atomic::Ordering, atomic_sc::AtomicI32, committer::Committer}; use std::thread; // TODO: Replace with the creusot_std version of thread diff --git a/src/solutions/ex3_parallel_add.rs b/src/solutions/ex3_parallel_add.rs index d5f07f3..b2de292 100644 --- a/src/solutions/ex3_parallel_add.rs +++ b/src/solutions/ex3_parallel_add.rs @@ -1,4 +1,3 @@ -use creusot_std::std::sync::atomic_sc::{AtomicI32, UpdateCommitter}; use creusot_std::{ ghost::{ invariant::{AtomicInvariantSC, Protocol, Tokens, declare_namespace}, @@ -7,7 +6,10 @@ use creusot_std::{ }, logic::{Id, ra::excl::Excl}, prelude::*, - std::thread::{self, JoinHandleExt}, + std::{ + sync::{atomic::Ordering, atomic_sc::AtomicI32, committer::Committer}, + thread::{self, JoinHandleExt}, + }, }; declare_namespace! { PARALLEL_ADD } @@ -58,7 +60,7 @@ pub fn parallel_add() -> i32 { ); thread::scope(|s| { - // We use move closure to make sure that they do not contain borrows of `Ghost<_>`, since + // We use move closures to make sure that they do not contain borrows of `Ghost<_>`, since // such a borrow would unnecesary consume space in these closures. So, we create the borrows // here. let mut frag1: Ghost<&mut _> = frag1.borrow_mut(); @@ -69,10 +71,10 @@ pub fn parallel_add() -> i32 { let t1 = s.spawn(move |tokens: Ghost| { atomic.fetch_add( 2, - ghost! { |c: &mut UpdateCommitter| { + ghost! { |c: &mut Committer<_, _, _, Ordering::SeqCst>| { inv.open(tokens.into_inner(), |inv: &mut ParallelAddAtomicInv| { inv.auth1.update(*frag1, snapshot!((Some(Excl(true)), Some(Excl(true))))); - c.shoot(&mut inv.own); + c.shoot_store(&mut inv.own); }) }}, ); @@ -81,10 +83,10 @@ pub fn parallel_add() -> i32 { let t2 = s.spawn(move |tokens: Ghost| { atomic.fetch_add( 2, - ghost! { |c: &mut UpdateCommitter| { + ghost! { |c: &mut Committer<_, _, _, Ordering::SeqCst>| { inv.open(tokens.into_inner(), |inv: &mut ParallelAddAtomicInv| { inv.auth2.update(*frag2, snapshot!((Some(Excl(true)), Some(Excl(true))))); - c.shoot(&mut inv.own); + c.shoot_store(&mut inv.own); }) }}, ); From 01ef36e418ff2566fabe07ff54a1725be59b3c0e Mon Sep 17 00:00:00 2001 From: Li-yao Xia Date: Fri, 17 Apr 2026 16:44:03 +0200 Subject: [PATCH 4/6] Fix unsoundness in creusot-std --- src/solutions/ex3_parallel_add.rs | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/src/solutions/ex3_parallel_add.rs b/src/solutions/ex3_parallel_add.rs index b2de292..293330e 100644 --- a/src/solutions/ex3_parallel_add.rs +++ b/src/solutions/ex3_parallel_add.rs @@ -71,9 +71,10 @@ pub fn parallel_add() -> i32 { let t1 = s.spawn(move |tokens: Ghost| { atomic.fetch_add( 2, - ghost! { |c: &mut Committer<_, _, _, Ordering::SeqCst>| { + ghost! { |c: &mut Committer<_, _, Ordering::SeqCst, Ordering::SeqCst>| { inv.open(tokens.into_inner(), |inv: &mut ParallelAddAtomicInv| { inv.auth1.update(*frag1, snapshot!((Some(Excl(true)), Some(Excl(true))))); + c.shoot_load(&inv.own); c.shoot_store(&mut inv.own); }) }}, @@ -83,9 +84,10 @@ pub fn parallel_add() -> i32 { let t2 = s.spawn(move |tokens: Ghost| { atomic.fetch_add( 2, - ghost! { |c: &mut Committer<_, _, _, Ordering::SeqCst>| { + ghost! { |c: &mut Committer<_, _, Ordering::SeqCst, Ordering::SeqCst>| { inv.open(tokens.into_inner(), |inv: &mut ParallelAddAtomicInv| { inv.auth2.update(*frag2, snapshot!((Some(Excl(true)), Some(Excl(true))))); + c.shoot_load(&inv.own); c.shoot_store(&mut inv.own); }) }}, From 0a0496688e9a3dc577b1590db6a651563d6cb69d Mon Sep 17 00:00:00 2001 From: Li-yao Xia Date: Mon, 20 Apr 2026 14:24:26 +0200 Subject: [PATCH 5/6] Bump Creusot version to 0.11.0 --- .github/workflows/ci.yaml | 2 +- Cargo.lock | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/.github/workflows/ci.yaml b/.github/workflows/ci.yaml index 1959884..5140419 100644 --- a/.github/workflows/ci.yaml +++ b/.github/workflows/ci.yaml @@ -11,7 +11,7 @@ concurrency: cancel-in-progress: true env: - CREUSOT_VERSION: v0.10.0+why3find-dep + CREUSOT_VERSION: v0.11.0 jobs: rust: diff --git a/Cargo.lock b/Cargo.lock index 3ae4605..6ac632d 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -10,7 +10,7 @@ checksum = "c08606f8c3cbf4ce6ec8e28fb0014a2c086708fe954eaa885384a6165172e7e8" [[package]] name = "creusot-std" -version = "0.11.0-dev" +version = "0.11.0" dependencies = [ "creusot-std-proc", "num-rational", @@ -18,7 +18,7 @@ dependencies = [ [[package]] name = "creusot-std-proc" -version = "0.11.0-dev" +version = "0.11.0" dependencies = [ "proc-macro2", "quote", From b5e650210076168aba9538762b8110e845875c6b Mon Sep 17 00:00:00 2001 From: Li-yao Xia Date: Wed, 22 Apr 2026 14:48:03 +0200 Subject: [PATCH 6/6] ci: Upgrade Creusot invocation in nightly run --- .github/workflows/nightly.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/nightly.yaml b/.github/workflows/nightly.yaml index ceafc47..e94d432 100644 --- a/.github/workflows/nightly.yaml +++ b/.github/workflows/nightly.yaml @@ -50,4 +50,4 @@ jobs: echo -e '[patch.crates-io]\ncreusot-std = { path = "../creusot/creusot-std" }' > .cargo/config.toml - name: Run Creusot - run: cargo creusot prove -- -Fsolutions + run: cargo creusot -- -Fsolutions