Re: Listing 9.2: actual free(3) will probably cause problem

["Paul E. McKenney" <paulmck@linux.vnet.ibm.com>]

On Sun, Oct 29, 2017 at 08:42:02PM +0900, Akira Yokosawa wrote:
> On 2017/10/29 09:19:07 +0800, Yubin Ruan wrote:
> > [Off list...]
> 
> Well, this was on the list. I'm keeping the CC.
> 
> > 
> > On 10/28/2017 09:12 PM, Paul E. McKenney wrote:
> >> On Sat, Oct 28, 2017 at 05:29:34PM +0800, Yubin Ruan wrote:
> >>> Hi Paul,
> >>>
> >>> I would suggest the following patch for defer/route_refcnt.c (as in Listing
> >>> 9.2). For the change in re_free, if we actually call free(3) on `rep', we will
> >>> lose that piece of memory so that the READ_ONCE() at line 36 might see garbage
> >>> value and will probably will not call abort(3), i.e., that is implementation
> >>> specific behavior. And I don't see why will we have `old <=0`.
> >>>
> >>> I think I understand what that code mean but you might mean some other?
> >>> Hopefully I will not be too picky.
> >>
> >> Yes, this code is buggy and fixing it is on my list.  I would be happy to
> >> accept a patch doing a real fix, but it is not simple.
> >>
> >> One place to start is Anthony Williams's atomic shared pointer code.
> >> The idea would be to translate that from C++ to C.
> > 
> > Can you provide some references?

https://bitbucket.org/anthonyw/atomic_shared_ptr

And, for completeness, a few others:

http://en.cppreference.com/w/cpp/experimental/atomic_shared_pt

https://isocpp.org/files/papers/N4162.pdf

Not so much a fan of this one because there really are already workloads
out there that need more than 48 bits of address space, but here you go:

https://github.com/facebook/folly/blob/master/folly/concurrency/AtomicSharedPtr.h

There have been quite a few papers published on this topic over the
past 20 years, most of which have at least one bug.  :-/

> >> But please be aware that this is a non-trivial problem.  If you try to
> >> hack together a solution, it -will- have subtle bugs.  So validating
> >> your solution (even if you start from Anthony's approach) will be
> >> non-trivial.  I suggest using cbmc or something similar in addition to
> >> perfbook's stress tests.
> >>
> >> So, are you up for it?  ;-)
> > 
> > Akira, can you provide some comments? I not sure what is wrong with my
> > suggestions. 
> 
> I think Paul didn't mean your suggestion was wrong. He wants formal
> verification of its correctness. And he might have noticed other issues
> in the code.
> 
> Paul, correct me if I'm guessing wrong.

You got it -- for this level of complexity and subtlety, formal verification
really is needed.

> > And I currently don't know use those test. I will work on it.
> 
> The update of perfbook pushed earlier today contains relevant topics
> in the "formal" chapter and bibliography.
> 
> This looks to me a good opportunity for you.

That indeed was one of my motivations for expanding on this chapter.  ;-)

I suggest starting with CBMC and Nidhugg.  CBMC is easier to use, so I
would start with that, but you might need Nidhugg for larger scenarios.

							Thanx, Paul

> Akira
> 
> > 
> > Yubin
> > 
> >>>
> >>> ----------------------------------------
> >>> diff --git a/CodeSamples/defer/route_refcnt.c b/CodeSamples/defer/route_refcnt.c
> >>> index 8a48faf..0d24e9d 100644
> >>> --- a/CodeSamples/defer/route_refcnt.c
> >>> +++ b/CodeSamples/defer/route_refcnt.c
> >>> @@ -36,7 +36,8 @@ DEFINE_SPINLOCK(routelock);
> >>>  static void re_free(struct route_entry *rep)
> >>>  {
> >>>  	WRITE_ONCE(rep->re_freed, 1);
> >>> -	free(rep);
> >>> +    /* Will not actually free it. Just use the `re_freed' as a flag */
> >>> +	/*free(rep);*/
> >>>  }
> >>>
> >>>  /*
> >>> @@ -50,7 +51,6 @@ unsigned long route_lookup(unsigned long addr)
> >>>  	struct route_entry **repp;
> >>>  	unsigned long ret;
> >>>
> >>> -retry:
> >>>  	repp = &route_list.re_next;
> >>>  	rep = NULL;
> >>>  	do {
> >>> @@ -65,8 +65,6 @@ retry:
> >>>  			if (READ_ONCE(rep->re_freed))
> >>>  				abort();
> >>>  			old = atomic_read(&rep->re_refcnt);
> >>> -			if (old <= 0)
> >>> -				goto retry;
> >>>  			new = old + 1;
> >>>  		} while (atomic_cmpxchg(&rep->re_refcnt, old, new) != old);
> >>>
> >>> --
> >>> To unsubscribe from this list: send the line "unsubscribe perfbook" in
> >>> the body of a message to majordomo@vger.kernel.org
> >>> More majordomo info at  http://vger.kernel.org/majordomo-info.html
> >>>
> >>
> > 
> > 
>