Repository navigation
Conversation
a92f9be to
fffa0b2
Compare
|
Instead of specifying the contents of the shared pointer using the big sep of a number of pieces that are indexed by natural numbers, have you considered having the user provide a single predicate indexed by |
I dont see how your proposal is any different from this PR:
That is exactly what the user provides currently, except the logically irrelevant difference between
That's exactly what the current invariant does, it holds the pieces that have not been given out yet. Definition sptrInv (id: CtrlBlockId) (Rpiece : nat -> Rep) (ownedPtr:ptr) (pieceOut : nat ->bool) :=
let ctrVal := countLN pieceOut allPieceIds in
(dataLoc id),, ctrOffset |-> atomic.R "long" 1 (Z.of_N ctrVal)
** (if (bool_decide (ctrVal = 0))
then emp
else dynAllocatedR ty ownedPtr
** ([∗ list] ctid ∈ allPieceIds,
if pieceOut ctid then pieceRight id ctid else ownedPtr |-> Rpiece ctid)).When the reference count hits 0, I dont see what we gain by asking the user to do big_sep of pieces manually in the instantiation: as far as I can see that would only make it harder to state and operate on the invariant, e.g. using wands when taking out pieces: the pieces may not be taken out in sequence. Perhaps you meant something else, in which case, it would be best if you sketch the changes in concrete Coq code (need not be complete or compile fully).
You can already do that, by choosing I can add many more test/example proofs to illustrate how the spec covers various use cases |
334eab5 to
6b22d5b
Compare
|
What I see in your proposal is that a user of the specification instantiates it by providing What I'm suggesting is that the user provides two predicates, let us call them |
|
Actually, Do you still see any issue that needs to be fixed by introducing |
|
Ok, I'd like Inlining
Yes. My issue is that if the user's data is split using fractions, the set of parameters is suggesting a different decomposition. I think the interface should be more neutral. I'd like to move the |
That is a fundamental constraint of shared_ptr in my opinion. The resource split here captures how to split the ownership of the payload in between all the shared_ptr objects that refer to it. As there can be at most
The interface is already neutral. Do you have any example of a usecase that cannot be handled with the current specs? |
|
@simon-skylabs and I have been thinking about this and put together #13 with our current thoughts. It is a slightly different abstraction of the shared_ptr specification, in certain examples that we have looked at, it seems a bit more flexible, but the heavy reliance on fractions might be a bit clunky. Have you gotten very far using the specifications in this PR? Have you run into any issues? I am pretty sure that we could prove this setup on top of the low-level interface in that spec, but I don't think that it would work well on top of the higher-level interface because of the fixed fraction accounting that you are doing here. |
I have not been able to find the time to work on the proofs that use shared pointers. I have had more important proof tasks come up and they do not use shared pointers. I looked at your PR and it seems strictly less general than this as it enforces splitting via fractions vs the approach here of letting the user chose arbitrary ways to split. I didn't comment there because there is nothing new to add beyond the discussion in this PR. |
|
Thanks, @aa755! I missed the asymmetric sharing protocol; however, I think that this means that the code that you are referencing is using the array specialization of shared pointer, right? That is a little bit different than the setup in the regular shared pointer implementation (at least because it uses |
Right, the code uses array specialization. Yes, the implementation would be slightly different ( Even when shared_ptr is used with a non-scalar, non-array object, e.g. some class instance, I think there will be many applications where clients may use the different shared ptr objects protecting the object to write to different parts of the object concurrently. the fractional splitting approach does not seem to be usable for these proofs. |
|
Perhaps you can start with the client-chosen splitting approach in this spec and then derive on top your fractional splitting spec. |
bb1dc62 to
430b828
Compare
… aa755/shared_ptr_squashed # Conflicts: # rocq-brick-libstdcpp/proof/dune.inc
Empty array slices hold at nullptr. Explicitly exclude null source and destination pointers even for zero-length calls, matching the C++23 library contract. Reported as SkyLabsAI#170. Checked the spec through Proof General and Dune.
…shed # Conflicts: # rocq-brick-libstdcpp/proof/dune.inc
Use the generated source translation unit and open std.atomic after its upstream namespace move. Keep the existing contracts and representations unchanged. The specs file checks to EOF in Emacs and compiles in the composed workspace build.
In the non-null branch, require the outstanding Rpiece at the pointee p rather than at the shared_ptr handle this. Preserve the null branch and the returned pieceRight token. Checked shared_ptr/specs.v to EOF through Emacs/Proof General and rebuilt monad/monadproofs/proofs/all.vo in the composed workspace. No client proof edits, new axioms, or admitted items.
Fraction the handle fields and structR only; keep acquisition tokens and payload pieces separate. Copy and accessors preserve arbitrary source fractions, while construction returns full ownership and move/destruction require it. Prove the fraction instances and a copy/destroy client regression under the existing assumed library specs. Port both existing examples to the current automation. Interactive checks passed for specs.v, both existing examples, the new regression, and Monad exec_specs.v. Dune built both example files. The central all.vo rebuild was interrupted before completion because a separately reviewed destruction-interface revision will change the same dependency; the final combined revision must pass that gate. No new axioms or admits.
Record the complete payload type, including array extent, in CtrlBlockId. Use that type for allocation tokens and reconstruction, with delete_compat connecting it to the public shared_ptr element type. Constructor specs return the actual allocation type. This prevents the array model from treating T[] as an allocated complete object. Both constructor examples now assert the exact managed type. Specs and examples check in Emacs; Dune built test.vo and fractional_copy.vo. No new axioms or admits. The full Monad build will be checked after the separate destruction-condition revision.
Replace the pure all-pieces-to-anyR condition with a persistent capability to run destruction of the complete managed type. This supports cancelling payload invariants and invoking nontrivial member destructors, while retaining the allocation token separately for deallocation. Constructor callers must establish the capability; it is not a new axiom. Port scalar/array constructor examples and prove guarded_int_destroy using existing cancellation and destruction rules. Keep the copy/destroy regression. Independent read-only review found no introduced blocker. Library operations remain assumed specs; this is not a proof of libstdc++ bodies or of VarCodeR. Validation: changed files checked interactively, test.vo and fractional_copy.vo built, the complete monad/monadproofs/proofs/all.vo build succeeded, and all.v checked through EOF in Emacs (locked-end 4034). No new axioms, admits, production C++ changes, or proof exclusions.
Define an auth_nat invariant owning the available exclusive piece rights. Prove allocation, take, refund, additive credit splitting, a reservation round-trip, and the capacity bound. Use existing ghost-state rules only; do not assume shared_ptr method specs or introduce axioms. Keep library protocol corrections separate.
Add the piece index to SharedPtrR and back it with fractional ghost ownership. Available indices retain their full witness in the invariant, including at zero count. Copy fixes the acquired index, moves preserve it, and destruction requires and refunds that index. Prove outstandingness and positive-count consequences independently of the assumed C++ method specs. Port scalar, array, and fractional-copy client tests without changing their proof bodies. No new axioms or admits. Validated interactively in Emacs and with dune build monad/monadproofs/proofs/all.vo and the shared_ptr/test.vo target in the composed workspace.
Replace the admitted capacity and incorrect 2^32 lower bound with a sealed definition of INT_MAX (2^31 - 1) and proved bounds. Check the _Atomic_word ABI in the include translation unit and document the finite outstanding-handle argument. Use a module lock rather than plain Opaque: vm_compute otherwise unfolds the capacity and can expand the billion-element ghost-token sequence. The existing constructor tests and fractional-copy regression check without proof-script changes; both new arithmetic lemmas are closed under the global context.
Model libstdc++'s _M_use_count as its actual raw int field rather than an abstract atomic<long> at an admitted offset. Keep physical counter and payload resources only in the positive-count invariant; prove that the retired invariant contains only ghost tokens. Document the remaining partial-control-block boundary and excluded weak_ptr operations. Shared-pointer implementation specs remain assumed. Checked fractional_copy, token_pool, and handle_liveness targets.
Replace the mandatory standalone payload allocation in sptrInv with an existential allocation case. Preserve public SharedPtrR parameters and the indexed copy-credit protocol. Default make_shared objects retain their enclosing allocation; array factories retain the backing allocation and the tail control-block placement token. Keep the existing separate new/new[] routes. Document that custom deleters, custom allocators, aliasing, overwrite factories, and external weak_ptr operations remain unsupported. No new axioms or factory specs; this is an allocation-component correction, not verification of the still-partial control-block model or C++ library bodies. Checked allocation, specs, and liveness interactively; allocation_test, fractional_copy, handle_liveness, and shared_ptr/test.vo build. Full Monad all.vo validation is running separately.
Require the actual construct_at specialization and payload destruction capability instead of assuming arbitrary constructor behavior. Preserve forwarded-argument effects and return the initial handle, payload piece, and bounded copy rights using the existing combined-allocation representation. Exclude enable_shared_from_this through an explicit inheritance guard, retain the array-factory and weak-pointer limitations, and test mutable, const, and rvalue calls. Prove the sample payload constructor, destructor, placement allocation, and linked construction obligation. Export payload_destructible opacity for clients. Validation: interactive spec and regression checks; monad/monadproofs/proofs/all.v checked to EOF in Emacs; all.vo built successfully. Final dependency build took 1241.290 seconds; new regression fixture took 333.571 seconds in that parallel build. (cherry picked from commit c0ed806)
Include __new_allocator ownership in allocator.R. Preserve the empty void and top-level cv-qualified specializations, and derive fractional laws without expanding the conditional through the generic derive tactic. This repairs the existing assumed allocator lifecycle interface; it adds no axiom. Checked the Intercode const conversion and the complete Monad all.vo suite. (cherry picked from commit 8da27b2)
Add the approved generic library interface for a nonempty fractional source and a distinct, possibly empty destination. Require acquisition of a new piece before returning the old destination's piece right. Keep self-assignment and empty sources outside this interface. Add a cpp.prog client regression; this does not verify the library implementation. The full Monad all.vo suite passes. (cherry picked from commit 427b0dd)
Let the verified construct_at obligation return an allocation-dependent descriptor, all pieces for its fixed recipe, and the matching destruction capability. make_shared returns a handle using exactly that descriptor and family; SharedPtrR, raw-pointer adoption, copy credits, and destruction interfaces are unchanged. Model libstdc++'s managed remove_cv_t<T> with top-level drop_qualifiers, preserving pointee constness. Document intentional disposal of placement-new metadata without discarding allocation ownership. Port the forwarding and constructor regressions and add a pointer-to-const factory client. Checked interactively in Emacs; Monad proofs/all.v checks to EOF and proofs/all.vo builds. No new axioms or admits. (cherry picked from commit f9f1402)
Reuse the tested dependency merge, taking upstream's memcpy preconditions and retaining the shared-pointer theory dependencies. Drop the obsolete local cstring goal-selector directive so the PR no longer changes that unrelated file.
(cherry picked from commit 76391a4)
(cherry picked from commit 3327240)
|
Updated to |
Decide the complete exported base graph with a finite worklist. Reject missing and opaque declarations instead of accepting an unknown hierarchy. Use the boolean in make_shared; defer automatic hints and dedicated checker cases as requested. PR: SkyLabsAI#10
Require shared_ptr_no_esftb in init_ctor, matching make_shared. Framing payload ownership unchanged is invalid when adoption initializes enable_shared_from_this. Array adoption is unchanged because it skips that initialization. PR: SkyLabsAI#10
Tie the subscript index to the complete managed array type recorded by the control block. Port both indexed writes in the existing array client. PR: SkyLabsAI#10
Require equivalent whole ownership, every live handle and unused right, and explicit invariant modality conditions. Retire the old ghost invariant and allocate a new protocol while preserving all physical handles, allocations, and the count. Prove a non-pointwise partition exchange regression for an equality-ordered SC index; add no axioms. PR: SkyLabsAI#10
Retain cleanup mode and allocation alignment through the control-block protocol and proved redistribution. Keep make_shared payload destruction separate from raw delete. Check class-specific scalar/array delete lookup and runtime effects; verify raw int clients against complete deletion obligations. PR: SkyLabsAI#10
Derive the null and nonnull specializations from the common contract. Prove fractional copy-and-destroy clients for both branches through ordinary spec discovery, without a null-only registered assumption. PR: SkyLabsAI#10
Retain cleanup mode and allocation alignment through the control-block protocol and proved redistribution. Keep make_shared payload destruction separate from raw delete. Check class-specific scalar/array delete lookup and runtime effects; verify raw int clients against complete deletion obligations. PR: SkyLabsAI#10
Derive the null and nonnull specializations from the common contract. Prove fractional copy-and-destroy clients for both branches through ordinary spec discovery, without a null-only registered assumption. PR: SkyLabsAI#10
Keep the implicit weak counter and an abstract layout remainder once in the shared invariant. Preserve that ownership during ghost-ID redistribution and check its exclusivity. The layout predicate and its Timeless law are explicit assumed library interfaces; no library-body correctness is claimed. Intended upstream destination: SkyLabsAI#10 (not yet published).
Keep the implicit weak counter and an abstract layout remainder once in the shared invariant. Preserve that ownership during ghost-ID redistribution and check its exclusivity. The layout predicate and its Timeless law are explicit assumed library interfaces; no library-body correctness is claimed. Intended upstream destination: SkyLabsAI#10 (not yet published).
|
Pushed the focused control-block ownership repair as The PR description now reflects these assumptions and limitations. Shared-pointer regressions, the const-conversion regression, and downstream CI for this commit failed before compilation: checkout of |
Scope
libstdc++ shared-pointer representations, explicitly assumed library method
specs, and proved supporting lemmas and client examples:
acquisition-token pool bounded by the signed
intstrong-reference counter.complete managed-object types.
make_shared.Both creation paths use the same payload-piece protocol. Raw adoption requires
a capability for the entire selected delete/delete[] operation; combined
factories require destruction only. The factory's constructor proof can
choose an allocation-dependent descriptor for its pieces.
Control-Block Ownership Repair, 2026-11-01
Commit
b750807adds the missing physical control-block ownership:_M_weak_count = 1andControlBlockLayoutR,alongside the existing strong counter, allocation ownership and payload pieces.
This ownership occurs once per control block, not once per shared handle.
ControlBlockLayoutRabstracts the remaining initialized fields, class/dispatchinformation and padding. It excludes both counters, payload and allocation
tokens. The predicate and its
Timelesslaw are new trusted declarations,not a proved concrete layout.
ghost IDs. An exclusivity regression checks that the full resource cannot be
duplicated. Constructors must establish the strengthened Rep; no rule creates
the new ownership from the old incomplete Rep.
This repairs the assumed interface, not libstdc++'s method bodies.
Additional Review Repairs, 2026-10-30
Two focused commits:
062f1537: raw adoption requirespayload_deletable, covering destruction,deallocation, and class-specific operator-delete effects. The selected
function is extracted from the exported libstdc++ delete expression, not
guessed from destructor metadata. Missing or unrecognized bodies fail the
selector. The handle retains selection evidence from a compatible TU and
records the allocation alignment; redistribution preserves both.
Combined factories retain destruction-only cleanup and never delete the
interior payload separately.
b5d03853: one registered copy-constructor spec covers empty and live sourcehandles. The old live contract and the empty contract are proved
specializations. Empty copying needs no acquisition token; a body-checked
copy-and-destroy client exercises normal spec discovery.
Regressions include scalar/array class-specific delete selection, retention of
that selection evidence by fractional handles, raw-adoption clients, and empty
copying. A native C++ test checks the class-specific deallocation effects and
that combined scalar/array factories do not invoke those operators. It passes
normally and with AddressSanitizer/UndefinedBehaviorSanitizer. This native array
test is not an array-factory Rocq spec. No new semantic axiom was added.
Review Repairs, 2026-10-29
Four focused commits:
787bc97: executableshared_ptr_no_esftb, with a proved equivalence toits complete-hierarchy exclusion predicate. The worklist has a proved finite
bound and handles repeated bases. Missing, unsupported, and opaque class
declarations fail the check; unavailable base information is not evidence
of absence.
make_sharedand its clients now use this boolean.8b2b39b: require the same exclusion in raw-pointer adoption, which otherwisecould modify the framed payload's internal weak handle. Array adoption
remains exempt because it skips that initialization.
b5a487a: array indexing requires the recorded complete managed typeTarray ety lenand0 <= index < len. The existing array client suppliesits actual length at both indexed writes.
4bf0fb3: replace the unrestricted admittedredistributePayloadOwnershipwith a proved migration. It requires equivalent whole-payload ownership,
every live handle and its piece, every unused acquisition right, at least
one live handle, and explicit
Timeless/WeaklyObjectiveconditions. Itretires the old invariant and returns a fresh ghost protocol with unchanged
physical handles, allocation, managed type, payload address and counter.
The regression moves integer ownership from index 0 to index 1, so it does
not require pointwise-equivalent pieces.
The redistribution regression uses an equality-ordered SC index. With other
thread-view orders, the allocation interface currently supplies no
weak-objectivity law; the general theorem keeps that caller obligation explicit.
No new axiom was introduced. Automatic checker hints and dedicated inheritance
checker examples are deferred; the proof of the decision procedure and existing
constructor clients are included.
Assumptions and Limits
The shared-pointer method specs remain assumed third-party interfaces.
The supporting proofs do not verify libstdc++'s method bodies or its actual
acquire/release synchronization. The ownership-transfer model uses SC invariant
reasoning; a weak-memory justification may require a different protocol.
The live invariant now owns both counters; the weak count is fixed at 1 under
the exclusion of external weak pointers. Remaining control-block layout ownership
is abstract:
ControlBlockLayoutRand itsTimelesslaw remain assumed. A bodyproof must define that layout, justify dispatch and combined-counter atomic
accesses, and recover combined-array layout/padding for deallocation.
Custom deleters/allocators, aliasing, weak-pointer interaction,
enable_shared_from_this, andmake_shared_for_overwriteare not supported. Array layouts are represented,but there is no
make_shared<T[]>factory spec in this PR.Branch and Validation
This focused branch excludes the
vector<bool>changes inPR #232. Its shared-pointer
sources match the combined development checkout.
The changed specs, raw-adoption tests, empty/live-copy examples, redistribution,
allocation, assignment, and factory regressions pass in the composed workspace.
The downstream
monad/monadproofs/proofs/all.vobuild and the separatetest/shared_ptr/const_conversion.voregression also pass. Revalidated on 2026-11-01 with development commitd6bafbd; the PR branch'sshared-pointer sources are identical. The downstream State destructor also
rebuilds. This is not a standalone build of every upstream package or a claim
that downstream proofs are free of inherited semantic assumptions.
Isolated library measurements on 2026-10-30, with one batch Rocq compilation at
a time and no observed activity in unrelated interactive Rocq workers:
specs.vtest.vfractional_copy.vredistribution.vThese replay Dune's compiler actions on identical temporary source copies, with
the same logical namespace and the existing command-level profiling wrapper.
Elapsed and instruction totals come from Rocq; peak RSS comes from Linux process
accounting. Major allocations include promotions, so the two word counts must
not be added. These are post-change measurements, not a before/after speedup
claim. The measured shared-pointer sources matched PR head
b5d03853. These measurementspredate the control-block ownership repair; they are not measurements of
b750807.The latest GitHub CI run for
b750807failed before compilation: the "Check out ci repository" step reported
Input required and not supplied: token. This is the CI workflow's checkoutcredential, not local GitHub authentication. Local results do not establish that
hosted CI passes.