Conversation
Based on discussion with @simon-skylabs.
|
Performance summary for https://github.com/SkylabsAI/brick-libcpp/actions/runs/19254124689
Full Results
|
| References can be combined according to the sum monoid and the sum | ||
| of all of the <<n : N>> will be the current value of the reference count. | ||
| *) | ||
| Parameter ref : gname -> N -> mpred. |
There was a problem hiding this comment.
Also need to expose the auth here (and make this fractional).
| Parameter ref : gname -> N -> mpred. | |
| Parameter ref : gname -> Qp -> N -> mpred. | |
| Parameter share_count : gname -> N -> mpred. |
|
|
||
| The [PR] ownership that is returned to the client are effectively lost forever; | ||
| however, because <<PR>> can be split arbitrarily it is always possible to get | ||
| more pieces by splitting the component that you have. The downside to this is |
There was a problem hiding this comment.
The downside to this is ...
I wouldn't call this a downside. I would phrase it as a simple observation. I don't think uniform fractions gets us anything but it's odd to not have it.
| 3. When destroying a shared_ptr, the <<PR qr>> is returned to the shared_ptr | ||
| abstraction and a [contender] token is returned to the caller. | ||
|
|
||
| The [PR] ownership that is returned to the client are effectively lost forever; |
There was a problem hiding this comment.
| The [PR] ownership that is returned to the client are effectively lost forever; | |
| The [PR] ownership that is returned to the client is effectively lost forever; |
There's an asterisk here. With use_count we can actually get all the ownership out.
There was a problem hiding this comment.
I am no longer convinced that this is sound sound due to issues noted next to the specification of use_count. It might still be, but the weak load is concerning.
|
|
||
| (** permits weakening of <<PR>>, this is subtle and might not be necessary *) | ||
| Axiom R_weaken : forall g PR PR' qr q p (_ : Fractional PR'), | ||
| (Forall q, PR q -* PR' q) |-- R g PR qr q p -* R g PR' qr q p. |
There was a problem hiding this comment.
I don't think this is sound. I think we need PR' q -* PR q instead: we're allowed to call the shared_ptr dtor on l_addr |-> shared_ptr.R g PR qr q p provided we also give up the ownership of p |-> PR qr. If we're allowed to weaken PR, we're making the dtor less demanding. If we start with PR qr := intR qr 7, we can weaken it to True and not have to return anything.
There was a problem hiding this comment.
Indeed! Good catch.
| ```coq | ||
| (** Ownership of the [shared_ptr] object carrying the pointer *) | ||
| Parameter R : gname -> cQp.t -> ptr -> Rep. | ||
| #[only(cfrac,cfracvalid,ascfractional,timeless)] |
There was a problem hiding this comment.
| #[only(cfrac,cfracvalid,ascfractional,timeless)] | |
| #[only(cfrac,cfracvalid,ascfractional,timeless)] derive R. |
|
Performance summary for https://github.com/SkylabsAI/brick-libcpp/actions/runs/19590796174
Full Results
|
3 participants
Notes about potential specifications for shared pointer.
Compared to #10, this approach goes a bit farther in separating out the pieces of the ownership in order to support some other patterns, but there are some subtlties in this design that will leak through to clients. The idea of establishing a low-level specification and then deriving a higher-level, more usable specification from it might be a good way to go; however, there are some subtleties because the standard seems to suggest that some operations in
shared_ptruse weak synchronization which would leak in the interface (BRiCk does not currently support this).