Skip to content

Operations on AtomicI32#1844

Merged
Lysxia merged 2 commits intocreusot-rs:masterfrom
dianegolfouse:atomics
Jan 9, 2026
Merged

Operations on AtomicI32#1844
Lysxia merged 2 commits intocreusot-rs:masterfrom
dianegolfouse:atomics

Conversation

@dianegolfouse
Copy link
Copy Markdown
Collaborator

No description provided.

Copy link
Copy Markdown
Collaborator

@jhjourdan jhjourdan left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Plenty of other atomic types and operations are missing, we should use a macro to generate specs for all of them.

Also, missing : at least one test.

Naming: what about renamig LocalInvariant -> ThreadInvariant (or something else like NonAtomicInvariant : I simply don't like LocalInvariant).

While I understand why you used a wrapper around AtomicI32 (and I somehow agree), I disagree with the idea of moving them to ghost::atomic_invariant. This has nothing to do with invariants, really. So we should either add a dedicated module or move this to std::sync::atomic (even though this is arguable because this is really a different type).

Comment thread creusot-contracts/src/ghost/atomic_invariant.rs Outdated
Comment thread creusot-contracts/src/ghost/atomic_invariant.rs Outdated
Comment thread creusot-contracts/src/ghost/atomic_invariant.rs Outdated
Comment thread creusot-contracts/src/ghost/atomic_invariant.rs Outdated
Comment thread creusot-contracts/src/ghost/atomic_invariant.rs Outdated
Comment thread creusot-contracts/src/ghost/atomic_invariant.rs Outdated
Comment thread creusot-contracts/src/ghost/atomic_invariant.rs Outdated
Comment thread creusot-std/src/ghost/invariant.rs
Comment thread creusot-contracts/src/std/thread.rs Outdated
@dianegolfouse dianegolfouse force-pushed the atomics branch 2 times, most recently from 90b37cb to fd95951 Compare December 2, 2025 13:09
@lafeychine lafeychine force-pushed the atomics branch 2 times, most recently from a9f04ca to ed83f1c Compare December 15, 2025 10:35
Comment thread creusot-std/src/ghost/invariant.rs
Comment thread creusot-contracts/src/ghost/invariant.rs Outdated
Comment thread creusot-contracts/src/ghost/invariant.rs Outdated
Comment thread creusot-contracts/src/ghost/invariant.rs Outdated
Comment thread creusot-contracts/src/ghost/invariant.rs Outdated
Comment thread creusot-std/src/ghost/invariant.rs
Comment thread creusot-contracts/src/ghost/invariant.rs Outdated
Comment thread creusot-contracts/src/std/sync.rs Outdated
Comment thread creusot-contracts/src/std/sync.rs Outdated
Comment thread creusot-contracts/src/std/sync.rs Outdated
Comment thread tests/should_succeed/atomics/parallel_add.rs Outdated
Comment thread tests/should_succeed/atomics/parallel_add.rs Outdated
Comment thread tests/should_succeed/atomics/parallel_add.rs Outdated
Comment thread tests/should_succeed/atomics/parallel_add.rs Outdated
Comment thread tests/should_succeed/atomics/parallel_add.rs Outdated
@jhjourdan
Copy link
Copy Markdown
Collaborator

If you agree, I think the current situation is acceptable.

@jhjourdan jhjourdan marked this pull request as ready for review January 7, 2026 14:14
@Lysxia Lysxia mentioned this pull request Jan 9, 2026
2 tasks
@lafeychine lafeychine force-pushed the atomics branch 6 times, most recently from 78fa642 to 7ac65f6 Compare January 9, 2026 14:10
@Lysxia Lysxia merged commit bbb7a0e into creusot-rs:master Jan 9, 2026
9 checks passed
@dianegolfouse dianegolfouse deleted the atomics branch February 14, 2026 09:55
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

4 participants