Conversation
CI summary (Details)Active Repos
|
| Repo | Job Branch | Job Commit |
|---|---|---|
| ./ | main | db1581e |
| fmdeps/BRiCk/ | main | e819c36 |
| fmdeps/auto/ | main | bc4c71e |
| fmdeps/auto-docs/ | main | 6490c5f |
| bluerock/NOVA/ | skylabs-proof | f3533d2 |
| bluerock/bhv/ | skylabs-main | e37df58 |
| fmdeps/ci/ | main | e1ec839 |
| vendored/elpi/ | skylabs-master | c0b9653 |
| vendored/flocq/ | skylabs-master | cf9cc84 |
| vendored/rocq/ | skylabs-master | bef7df5 |
| fmdeps/rocq-agent-toolkit/ | main | 227bb83 |
| vendored/rocq-elpi/ | skylabs-master | 7dee592 |
| vendored/rocq-equations/ | skylabs-main | 9cf8471 |
| vendored/rocq-iris/ | skylabs-master | a7af9f7 |
| vendored/rocq-lsp/ | skylabs-main | 64ef78a |
| vendored/rocq-stdlib/ | skylabs-master | 00897b3 |
| vendored/rocq-stdpp/ | skylabs-master | 0c5e505 |
| fmdeps/skylabs-fm/ | main | 5c3d0ab |
| vendored/vsrocq/ | skylabs-main | ee79e7a |
Changes in Warnings or Errors
| Before | New | Fixed | After | |
|---|---|---|---|---|
| Errors | 0 | 0 | 7 | |
| Warnings | 91 | 91 |
Performance
| Relative | Master | MR | Change | Filename |
|---|---|---|---|---|
| +0.96% | 198198.0 | 200098.2 | +1900.2 | total |
| -0.52% | 1048.1 | - | -1048.1 | ├ disappeared files (13) |
| +1.46% | - | 2936.7 | +2936.7 | ├ newly appeared files (10) |
| +0.01% | 197149.8 | 197161.5 | +11.7 | └ common files |
| -0.00% | 53108.6 | 53108.4 | -0.2 | ├ translation units |
| +0.01% | 144041.3 | 144053.2 | +11.9 | └ proofs and tests |
Full Results
| Relative | Master | MR | Change | Filename |
|---|---|---|---|---|
| +41.01% | 31.2 | 44.0 | +12.8 | fmdeps/brick-libcpp/rocq-brick-libstdcpp/proof/mutex/spec/mutex.v |
| +0.96% | 198198.0 | 200098.2 | +1900.2 | total |
| -0.52% | 1048.1 | - | -1048.1 | ├ disappeared files (13) |
| +1.46% | - | 2936.7 | +2936.7 | ├ newly appeared files (10) |
| +0.01% | 197149.8 | 197161.5 | +11.7 | └ common files |
| -0.00% | 53108.6 | 53108.4 | -0.2 | ├ translation units |
| +0.01% | 144041.3 | 144053.2 | +11.9 | └ proofs and tests |
Fix invariant. Add specs for all functions in MyMutex. Not sure if we need do_store_C or do_load_C.
…ece of exclusive my_mutex
mutex.v now depends on a ghost state module defined in lock_ghosts2.v instead of the user ghost state. The usage is demonstrated in custom_mutex_hpp_proof.v. It has 3 pieces: - my_mutexes records the set of invariant gnames acquired by a thread, and should be allocated by spawn(). A singleton set should be given to a mutex invariant in exchange for the protected resources in it. - a pair of token/given_token. A thread acquiring the resource stores a fraction of token inside the invariant and gets back the same fraction of given_token; destructing lock requires the entire token and thus no thread can hold the lock. - a o_owner_tid, recording the thread ID of the current lock owner. The auth piece is in inv and frag is held by the current lock owner.
of the spec module.
pgiarrusso-sl
force-pushed
the
ke/mutex_impl
branch
from
September 10, 2026 16:07
e4cbb0f to
250308e
Compare
| (mp : ptr * mutex.gname * Qp * Qp) (q : cQp.t) (P : mpred) : Rep := | ||
| structR "std::lock_guard<std::mutex>" q ** | ||
| let '(mp, g, q') := mp in | ||
| let '(mp, g, q', _) := mp in |
Contributor
There was a problem hiding this comment.
Why are we adding a fraction that we're throwing away.
CI summary (Details)Active Repos
|
| Repo | Job Branch | Job Commit |
|---|---|---|
| ./ | main | db1581e |
| fmdeps/BRiCk/ | main | e819c36 |
| fmdeps/auto/ | main | 0d2d68d |
| fmdeps/auto-docs/ | main | 6490c5f |
| bluerock/NOVA/ | skylabs-proof | f3533d2 |
| bluerock/bhv/ | skylabs-main | e37df58 |
| fmdeps/ci/ | main | e1ec839 |
| vendored/elpi/ | skylabs-master | c0b9653 |
| vendored/flocq/ | skylabs-master | cf9cc84 |
| vendored/rocq/ | skylabs-master | bef7df5 |
| fmdeps/rocq-agent-toolkit/ | main | 227bb83 |
| vendored/rocq-elpi/ | skylabs-master | 7dee592 |
| vendored/rocq-equations/ | skylabs-main | 9cf8471 |
| vendored/rocq-iris/ | skylabs-master | a7af9f7 |
| vendored/rocq-lsp/ | skylabs-main | 64ef78a |
| vendored/rocq-stdlib/ | skylabs-master | 00897b3 |
| vendored/rocq-stdpp/ | skylabs-master | 0c5e505 |
| fmdeps/skylabs-fm/ | main | 5c3d0ab |
| vendored/vsrocq/ | skylabs-main | ee79e7a |
Changes in Warnings or Errors
| Before | New | Fixed | After | |
|---|---|---|---|---|
| Errors | 0 | 0 | 7 | |
| Warnings | 91 | 91 |
Performance
| Relative | Master | MR | Change | Filename |
|---|---|---|---|---|
| +0.96% | 198220.5 | 200120.6 | +1900.1 | total |
| -0.52% | 1048.2 | - | -1048.2 | ├ disappeared files (13) |
| +1.46% | - | 2936.7 | +2936.7 | ├ newly appeared files (10) |
| +0.01% | 197172.3 | 197183.9 | +11.7 | └ common files |
| -0.00% | 53108.6 | 53108.4 | -0.2 | ├ translation units |
| +0.01% | 144063.7 | 144075.6 | +11.9 | └ proofs and tests |
Full Results
| Relative | Master | MR | Change | Filename |
|---|---|---|---|---|
| -1.95% | 51.3 | 50.3 | -1.0 | fmdeps/brick-libcpp/rocq-brick-libstdcpp/proof/mutex/proof/unique_lock_recursive_mutex.v |
| +41.01% | 31.2 | 44.0 | +12.8 | fmdeps/brick-libcpp/rocq-brick-libstdcpp/proof/mutex/spec/mutex.v |
| +0.96% | 198220.5 | 200120.6 | +1900.1 | total |
| -0.52% | 1048.2 | - | -1048.2 | ├ disappeared files (13) |
| +1.46% | - | 2936.7 | +2936.7 | ├ newly appeared files (10) |
| +0.01% | 197172.3 | 197183.9 | +11.7 | └ common files |
| -0.00% | 53108.6 | 53108.4 | -0.2 | ├ translation units |
| +0.01% | 144063.7 | 144075.6 | +11.9 | └ proofs and tests |
…ic to implementation; add my_mutexes allocation rule and mutex invariant initalization rule
| (** Specialize the reusable specs to the standard mutex representation and | ||
| bind them to their C++ names. *) | ||
| Module StdMutex (Preds : MUTEX_PREDS with Definition cpp_ty := "std::mutex"%cpp_type). | ||
| Include Preds. |
Contributor
There was a problem hiding this comment.
Worth a closer look.
| Include Preds. | ||
| #[global] Hint Opaque token not_locked locked R : sl_opacity. | ||
|
|
||
| Module Spec := mutex_spec Preds. |
Contributor
There was a problem hiding this comment.
Worth a closer look.
|
|
||
| Initializing [this |-> R old 1$m emp] probably depends on the mutex | ||
| implementation. *) | ||
| Parameter init_R : forall (this : ptr) (old : gname) |
Contributor
There was a problem hiding this comment.
Conventionally, things in Prop are Axiom and things in Type are Parameters.
Suggested change
| Parameter init_R : forall (this : ptr) (old : gname) | |
| Axiom init_R : forall (this : ptr) (old : gname) |
| (** Register a thread by consuming its handle for this mutex's namespace | ||
| and its token share. [my_mutexes_alloc_mutex_name] splits this handle | ||
| from the full namespace pool supplied when the thread is spawned. *) | ||
| Parameter register_thread : forall |
Contributor
There was a problem hiding this comment.
Suggested change
| Parameter register_thread : forall | |
| Axiom register_thread : forall |
| try_lock_lockable cpp_ty (fun q gP => R gP.1 q gP.2). | ||
|
|
||
| Lemma try_lock_spec_equiv_try_lock_spec_alt | ||
| (Htry_lock : requirements.do_try_lock cpp_ty = do_try_lock) this xs K : |
Contributor
There was a problem hiding this comment.
Htry_lock seems odd — this should just be unfolding mutex_lockable?
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Conflicts with #167; maybe easiest to cherry pick from #167 and then close #167 at this point.
Currently, only rocq-brick-libstdcpp/proof/mutex/spec/mutex.v and rocq-brick-libstdcpp/test/mutex/custom_mutex_hpp_proof.v compile.
There are so many commits, and it might be easier to review the diff of the two branches instead of reading the commits.
The changes mostly include these aspects:
not_lockedincludes points-to ofm_owner, and it needs to be exposed during verification.lock_ghost2.v, see comments in the file for how these modules work):my_mutexesfor making sure a thread only gets resource once from a mutex invariant before itunlocks.