specs of shared_ptr

[aa755]

this PR also has the changes from #6 because there branch of that PR is not in this repo so I cannot select it as the base branch.
One way to ignore those already reviewed changes is to just look at the last commit

[simon-skylabs]

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 N and which starts at 0? The array use case that you sketch would be supported by instantiating that predicate with the big sep of pieces that haven't been given out yet. That would also allow a different instantiation where we instantiate the user predicate with something that admits fractional splitting.

[aa755]

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 N and which starts at 0? The array use case that you sketch would be supported by instantiating that predicate with the big sep of pieces that haven't been given out yet. That would also allow a different instantiation where we instantiate the user predicate with something that admits fractional splitting.

I dont see how your proposal is any different from this PR:

the user provide a single predicate indexed by N and which starts at 0

That is exactly what the user provides currently, except the logically irrelevant difference between N and nat: Rpiece: nat -> Rep. SharedPtr is just parametrized by Rpiece. The index does start at 0. Rpiece 0 is currently framed away from the init_ctor spec. From that, we can derive a spec stated in the way described in long description at the start of spec.v: the client deposits all the pieces and gets back the 0th piece. I added more comments to the init_ctor spec.

The array use case that you sketch would be supported by instantiating that predicate with the big sep of pieces that haven't been given out yet.

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, dynAllocatedR all the pieces will be taken out to satisfy the delete precondition.

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).

That would also allow a different instantiation where we instantiate the user predicate with something that admits fractional splitting.

You can already do that, by choosing Rpiece:= fun n => objR (1/maxContention)

I can add many more test/example proofs to illustrate how the spec covers various use cases

[simon-skylabs]

What I see in your proposal is that a user of the specification instantiates it by providing Rpiece as well as a maximum number of pieces and the spec itself takes the big sep of all the pieces.

What I'm suggesting is that the user provides two predicates, let us call them Rwhole : N -> Rep and Rpiece : N -> Rep which satisfy the equation forall n, Rwhole n -|- Rwhole (n+1) * Rpiece n. We don't need maxContention. If the user wants the array example, they instantiate Rwhole with a big sep. If they want a fraction, they use the appropriate ghost state and they then have a Rpiece which can be subdivided as much as desired. That would remove the maxContention limit from the specification and make it more agnostic to the way the user may want to use it.

[aa755]

Actually, maxContention is not chosen by the user: it is not a parameter/with-argument of any spec. It is a constant chosen by the implementation: it will be chosen to be the max value of the reference counter, e.g. 2^32 on 32 bit machines and 2^64 on 64 bit machines. Via maxContentionLb, the spec guarantees that all implementations allows counts to go up to 2^32-1 at least. We can actually get rid of maxContention and hardcode it as 2^64 (who uses 32 bit machines these days anyway), or derive it from the word size stored in genv.

Do you still see any issue that needs to be fixed by introducing Rwhole? I dont see why the user should be asked to make another choice (not just Rpiece but also Rwhole).

[simon-skylabs]

Ok, I'd like maxContention and the ownership of the user resource to be better separated then. maxContention is a limit on the number of times that the counter can be incremented, it has nothing to do with how much the resource can be split.

Inlining maxContention with a specific value does not address my concern. We can keep it abstract if different implementations choose different values for it or use a definition with a specific value in the specification if the same value is used everywhere. It shouldn't be hard to go from one to the other if we want.

Do you still see any issue that needs to be fixed by introducing Rwhole? I dont see why the user should be asked to make another choice (not just Rpiece but also Rwhole).

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 big_sepL to the user side.

[aa755]

Ok, I'd like maxContention and the ownership of the user resource to be better separated then. maxContention is a limit on the number of times that the counter can be incremented, it has nothing to do with how much the resource can be split.

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 maxContention live shared_ptr objects at any given time (otherwise the counter will overflow), there can bet at most maxContention pieces.

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 big_sepL to the user side.

The interface is already neutral. Do you have any example of a usecase that cannot be handled with the current specs?
You can easily do fractional pieces, and the number of actually relevant pieces need not be macContention. For example, you can do Rpiece := fun n => if decide (n<5) then objR (1/5) else emp, if in an application you only need to ever have 5 live shared_ptr objects refering to the payload.

[gmalecha-at-skylabs]

@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.

[aa755]

@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.

[gmalecha-at-skylabs]

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 delete[] rather than delete).

[aa755]

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 delete[] rather than delete).

Right, the code uses array specialization. Yes, the implementation would be slightly different (delete[] v delete), but I think the spec can be unified using anyR or some very localized matching on type, like we did for overhead in #11.

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.

[aa755]

Perhaps you can start with the client-chosen splitting approach in this spec and then derive on top your fractional splitting spec.