Page MenuHomePhabricator

[nofree] Attempt to further refine concurrency/capture requirements
AbandonedPublic

Authored by reames on Fri, Apr 16, 11:55 AM.

Details

Summary

Triggered by discussion on https://reviews.llvm.org/D100141.

Key changes:

  1. Reorder and use consistent wording to indicate what is specification, and what is discussion.
  2. Add the requirement for a nocapture parameter to the deref discussion. Without it, the old wording left it unclear whether the callee could capture a pointer, and then arrange for another thread to free it, while still being nofree. (I think the answer must be yes, as otherwise, we have to prove nocapture to prove nofree.)

One gap I still see - and don't have a great suggestion on how to fix - is whether a nofree function is allowed to free an object allocated by a different thread *after* the start of execution of 'f'. I think the answer should probably be no, I'm just not sure how to specify that in the wording.

Note that we don't currently implement the discussed deref rule, so there's no code to match this against or fix.

Diff Detail

Event Timeline

reames created this revision.Fri, Apr 16, 11:55 AM
reames requested review of this revision.Fri, Apr 16, 11:55 AM
Herald added a project: Restricted Project. · View Herald TranscriptFri, Apr 16, 11:55 AM

I think the crux of the discussion is the second half of this sentence:

A nofree function is explicitly allowed to free memory which it (or a transitive callee) allocated or (if not nosync) arrange for another thread to free memory on its behalf.

I'm trying to figure out whether that second half makes sense by analogy with other attributes. For example, consider a function that is inaccessiblememonly. Is such a function allowed to use the inaccessible memory to communicate with another thread which then touches memory that is accessible to the caller? I'm pretty sure the assumption in existing LLVM code is that the answer is "no".

But now, the equivalent question for nofree is answered "yes".

This inconsistency worries me.

In the original review D10041, @reames wrote:

To the best of my reading of the current code and specification, no having another thread free an object on the behalf of 'f' does not violate a nofree annotation on 'f'. The reasoning here is that a) 'f' is not the one actually freeing, and b) it we picked anything else as a semantic, inferring nofree would require concurrency aware full program analysis.

Is that full program analysis really required? Looking again at the analogy with inaccessiblememonly, it seems to be conservatively correct to say that a function that may communicate with another thread cannot be inaccessiblememonly. For example, a function containing an atomicrmw instruction cannot be inaccessiblememonly. The same argument should apply to nofree as well.

The question is then whether we believe that this would be too conservative for the goal of nofree. My gut feeling is that it isn't too conservative, but admittedly I haven't spent a lot of time thinking about it. In any case, there is still the seeming inconsistency between nofree and other attributes, which feels likely to cause problems further down the road (e.g., developers forgetting a check against nosync somewhere).

Assuming no new and strong arguments to the contrary, I would prefer that nofree works like older attributes such as inaccessiblememonly in this regard.

I think the crux of the discussion is the second half of this sentence:

A nofree function is explicitly allowed to free memory which it (or a transitive callee) allocated or (if not nosync) arrange for another thread to free memory on its behalf.

I'm trying to figure out whether that second half makes sense by analogy with other attributes. For example, consider a function that is inaccessiblememonly. Is such a function allowed to use the inaccessible memory to communicate with another thread which then touches memory that is accessible to the caller? I'm pretty sure the assumption in existing LLVM code is that the answer is "no".

The honest truth is that our concurrency specification, and in particular, how it interacts with attributes is lacking to say the least.

The case you raise is an interesting one. Current code clearly assumes that such writes would not be well defined (note I carefully did not say can't happen), but as you point the specification isn't terrible clear.

I do want to note that inaccessiblememonly is a bit of a weird cornercase (precisely because it's modeling access to things outside the model). We don't e.g. have a corresponding problem with readonly because synchronization must involve a write. (We model all ordered atomics as being writes, even the ones which only read. For exactly this reason.)

Longer term, it might very well be reasonable to allow readonly functions with ordered atomic loads. We'd simply have to a) specify the change, b) infer nosync, and c) update *all* users to check both attributes. The value would be in getting stronger aliasing results for uncaptured memory passed to a nocapture argument of a function which only read synchronizes. Seems like a pretty minimal value. Note that I'm not actively proposing doing this or volunteering for the work involved.

But now, the equivalent question for nofree is answered "yes".

This inconsistency worries me.

In the original review D10041, @reames wrote:

To the best of my reading of the current code and specification, no having another thread free an object on the behalf of 'f' does not violate a nofree annotation on 'f'. The reasoning here is that a) 'f' is not the one actually freeing, and b) it we picked anything else as a semantic, inferring nofree would require concurrency aware full program analysis.

Is that full program analysis really required? Looking again at the analogy with inaccessiblememonly, it seems to be conservatively correct to say that a function that may communicate with another thread cannot be inaccessiblememonly. For example, a function containing an atomicrmw instruction cannot be inaccessiblememonly. The same argument should apply to nofree as well.

The question is then whether we believe that this would be too conservative for the goal of nofree. My gut feeling is that it isn't too conservative, but admittedly I haven't spent a lot of time thinking about it. In any case, there is still the seeming inconsistency between nofree and other attributes, which feels likely to cause problems further down the road (e.g., developers forgetting a check against nosync somewhere).

Assuming no new and strong arguments to the contrary, I would prefer that nofree works like older attributes such as inaccessiblememonly in this regard.

I'll be honest, I'm not terrible a fan of nofree and nosync being split the way they are either. I find it confusing. However, that was clearly the intent of the original introduction, and nosync serves effectively no other purpose. If you want to propose (on llvm-dev) a change to this semantic, feel free. I'm not motivated to do so as what we have works well enough and is a reasonable solution to the problem space. Not necessarily the best, but a reasonable one.

I'm not a fan of this semantics either. nofree should mean nofree (transitively).
A nofree function shouldn't be able to pass a pointer to another thread and get it freed.

The condition should be: deref before call + nofree call => deref after call. Anything else is too complicated (and very surprising given the name "no free").
nosync should be used when inferring nofree instead.

llvm/docs/LangRef.rst
1616

this sentence wasn't finished.

I need some help figuring out how to make progress on nofree and related deref pieces. The comments on this review seem to focus mostly on the split between nofree and nosync. That split is existing in the LangRef today. I'm sympathetic to the view that wasn't the right choice, but it's what we have. I've already taken a pretty big detour from the thing I'm actually interested in working on (deref), and am not really interested in signing up for further redefinition of existing attributes.

Are we willing to live with the existing nofree vs nosync split or at least defer any potential redefinition to the future? If so, I'll abandon this review (because I just don't care that much about the capture point). If not, I'm probably going to declare the attempt at redefining deref to be a failure and stop work here. I'm open to suggestions to split the difference (i.e. is there a finite subset which lets us make progress you see?), but at the moment, I'm feeling pretty stuck.

Apologies if this is obvious somehow, but could you please point at those "deref" changes? I think I missed that part of the conversation. My hope would be that it could be treated orthogonally to the nofree/nosync question.

Apologies if this is obvious somehow, but could you please point at those "deref" changes? I think I missed that part of the conversation. My hope would be that it could be treated orthogonally to the nofree/nosync question.

Please see the llvm-dev thread "RFC: Decomposing deref(N) into deref(N) + nofree" for background. Note that the described nofree semantics in that first email have been since decided not to be correct, but it should give you a feel for the interactions.

I tried my hands at a change in the opposite direction in D101701

reames abandoned this revision.Wed, May 5, 12:33 PM

Abandoning as we seem to be converging on the alternative proposal.