[cfe-dev] Next step

[Delesley Hutchins]

[Ongoing discussion on thread safety analysis, moved to list in case
anyone cares.  :-)]

> * change getMutexIDs so that it creates an LExpr instead of a set of
> SExprs. Instead of returning a MutexIDList, it should return the LExpr
> created.

Yes.

> * addLock should be changed to take an LExpr instead of a MutexIDList
> (same for removeLock)

Yes.

> * FactSet needs to be updated to handle LExprs for findLock, addLock
> and removeLock

Yes, but there's more to it.  (See below.)

> * FactManager needs to create a FactID from an LExpr for newLock

Not quite.  (See below.)

> * FactEntry needs to be updated to hold (a union including SExpr and?) an LExpr

Not quite.  (See below.)

A few notes on implementation:  MutexIDList is just a short list of
SExprs, and it's used when extracting SExprs from attributes, because
an attribute (e.g. exclusive_locks_required) can hold a list of
SExprs, rather than a single one.

FactSet holds a set of SExprs that are known to be held.  It's not
just a list for two reasons.  (1) A FactSet keeps track of some
additional information about each SExpr, e.g. where the SExprs were
acquired, whether they are exclusive or shared, and the weirdness
associated with scoped_lockable.  (2) FactSets are optimized for small
size and merging.

You will need to change FactSet so that it holds a single LExpr.
Instead of the set {A, B, C},  you will store the LExpr  (A & B & C).
What this means is that the operations to add locks, remove locks, and
merge locksets will now apply to LExprs.
For example:

   Current context:  (A & B & !C).    Call  C.lock().   New context:
(A & B & C).
   Current context:  (A & B & C).     Call  B.unlock().  New context:
(A & C & !B).
   Context1:  (A & B & C).    Context2:  (A & B & D).   Merge on join
point:  (A & B & (C | D))

[Joint points].  At every join point in the CFG, the analysis will
have to merge the two LExprs.  Merging is conceptually simple:  if we
can arrive at a given basic block from either block 1, with context
E1, or from block 2, with context E2, then the context for that block
is (E1 | E2).   However, you will get an exponential blowup in
expression size unless you *simplify* (E1 | E2) afterward, as shown
above.

[Adding and removing locks.]  In order to add or remove a mutex A from
an LExpr E, you must first remove all prior occurrences of A from E.
(We're chan do not know ging what we know about A.)  Unfortunately,
that's not just a simple matter of traversing E, and deleting the
references.  You need to derive a new expression E' which does not
mention A, where E is satisfiable only if E' is satisfiable.  More
formally, you must factor out A, by refactoring E into the form  (A &
E1) | (!A & E2), where E1 and E2 do not refer to A;  E' is then (E1 |
E2).  There are algorithms to do this for BDDs; the operation is known
as boolean existential quantification. See:
http://gauss.ececs.uc.edu/Courses/c626/lectures/BDD/bdd-desc.pdf

Unfortunately, I do not know how to do this for the simple LExprs that
you have constructed.  One option is to require the LExpr to be in the
format  (E1 & E2 ... En & A)  to start with (so no refactoring
necessary), and simply fail otherwise.  That will work for locks,
because it matches the way FactSet is implemented now, and it will
thus allow you to make forward progress.  But it largely defeats the
point of implementing LExprs, since analysis will fail if it
encounters anything more complicated than what we already have.  The
other option is to ditch LExprs, and implement BDDs. Talk to Dean; he
knows more about this than I do.

My task list, in order of priority, would be:

(1) Add the ability to merge (logical or) and simplify LExprs.
(convert to conjuctive normal form?)
(2) Add the existential quantification operation to LExprs  (or
possibly implement BDDs?).
(3) Augment LExprs so that they keep track of exclusive vs. shared,
where locks were acquired, and scoped_lockable.

That's quite a lot of work already, and it will take you some time.
Once it's done, *then* we can do a single patch to swap FactSet over
to the new LExpr stuff.  The patch sequence is the same as my strategy
for the TIL/SExpr stuff; build the new functionality in parallel with
the old, make sure the new functionality works, and then flip the
switch from old to new.  Notice that I haven't flipped the switch for
SExpr yet.  :-)

We can set up a video chat if you want to talk about this further.

  -DeLesley

-- 
DeLesley Hutchins | Software Engineer | delesley at google.com | 505-206-0315