This project is read-only.

Eliminating the TLS mechanism

Jun 16, 2010 at 7:42 AM

Hi,

Mark mentioned to me that we could safely ditch the thread local storage support that was built into VCC because we now have better mechanisms to achieve this. Anybody disagree?

Stephan

Jun 16, 2010 at 7:53 AM
Hi, is there any documentation of these alternative mechanisms (I looked on the TLS wiki page but there is nothing mentioned), or could anyone please shortly comment on how to achieve TLS without the builtin primitive? Thanks, Thorsten
Jun 16, 2010 at 9:57 AM
Edited Jun 16, 2010 at 10:00 AM

[Update: message reedited using FF instead of Chrome...]

Hi Thorsten,

other than the things added explicitly by axioms (things being always closed to a certain thread), vcc(thread_local_storage) protects volatile fields from changing after the atomic havoc.

The alternative is approval, i.e., making use of VCC's "approves" macro. Unfortunately there's currently no Wiki page on this. I might try to dig out some from the ML archives later... There is a set of test cases in the VCC SVN repo, which you can find under "vcc/test/testsuite/vcc2/volatileVersion". Here is a short summary how it compares to vcc(thread_local_storage).

You can declare a volatile field "f" owner-approved by inserting the invariant "invariant(approves(owner(this),f)". If the current thread "me()" is the owner of a structure with such an invariant, it effectively keeps other thread from updating the variable (while they can still read it) - think of "single writer / multiple reader"-type of variables. In particular, the current thread can rely on the volatile field not being changed by atomic havoc at the beginning of atomic statements. Below, I've adapted the TLS examples from "vcc/test/testsuite/vcc2/tls" to the other style. As you can see, the axioms are gone and the TLS structure is passed around explicitly in ownership of the current thread (YMMV). A more subtle change is that in the last testcase the 3-element has been changed to a map and made a ghost structure -- "approves(o,f)" can be used only for primitive fields "f" (which can be worked around by adding shadow fields), we might consider making it more general, but it hasn't been much of a nuisance in real examples (if it's a ghost fields, maps might be preferable anyway).

Hope that helps, Mar

P.S.: my rich-text controls seems to be gone :| I'm pasting that file verbatim in here...

#include <vcc.h>

struct FooBar {
  int x;
};

struct FooBar g_FooBar;

struct vcc(volatile_owns) TLS_DATA {
  int dummy;
  spec(volatile bool f1;)
  invariant(approves(owner(this),f1))
  

  invariant(f1 ==> set_in(&g_FooBar, owns(this)))
};

void foo(struct TLS_DATA *d)
  maintains(wrapped(d))
  maintains(d->f1)
  writes(d)
{
  spec(
    atomic (d) {
      giveup_closed_owner(&g_FooBar, d);
      d->f1 = false;
	  bump_volatile_version(d);
    }
  )
  unwrap(&g_FooBar);
  g_FooBar.x = 10;
  wrap(&g_FooBar);

  spec(
    atomic (d) {
      set_closed_owner(&g_FooBar, d);
      d->f1 = true;
	  bump_volatile_version(d);
    }
  )
}

void shouldFail(struct TLS_DATA *d claimp(c))
  always(c,closed(d))
{
  assume(d->f1);
  atomic (c, d) {
    assert(d->f1);
  }
}
`
Verification of TLS_DATA#adm succeeded.
Verification of foo succeeded.
Verification of shouldFail failed.
testcase(48,14) : error VC9500: Assertion 'd->f1' did not verify.
`
`
#include "vcc.h"

typedef struct t{
  volatile bool flag;
  spec(volatile bool arr[unsigned];)
  invariant(approves(owner(this),flag))
  invariant(approves(owner(this),arr))
}t, *pt;

void f(pt tls)
	maintains(wrapped(tls))
	maintains(tls->flag)
{
  spec(bool temp;)

  atomic(tls){
    assert(tls->flag);
    begin_update();
    spec(temp = tls->flag;)
  }
}

void d(pt tls)
maintains(wrapped(tls))
maintains(tls->flag)
maintains(forall(unsigned int i; i < 3 ==> tls->arr[i])) // TODO
{
  spec(bool temp;)
  atomic(tls){
    assert(tls->flag);
    assert(forall(unsigned int i; i < 3 ==> tls->arr[i]));
    begin_update();
    spec(temp = tls->flag;)
  }
}

`
Verification of f succeeded.
Verification of d succeeded.
`

Jun 16, 2010 at 10:19 AM
Edited Jun 16, 2010 at 10:20 AM

Hi Mark,

thank you very much for the detailed explanation and that you took the time to convert the TLS examples to the new approver-approach.

I guess that you could also add the TLS-axioms again in the approver approach if you really wanted to, so that would be orthogonal to preserving the values of owner-approved volatile variables in atomic blocks, right?

Thorsten

[edit: lets see if chrome instead of FF likes my linebreaks]

Jun 16, 2010 at 11:43 AM
Hi Thorsten, yes you might want to use the axioms as well. Though, to take advantage of thread-approval (i.e. "invariant(approves(owner(this),this))" where "owner(this)" is of thread type -- otherwise approves() is no different from "unchanged(f) || inv2(owner(this))" in VCC) you might want to extend to not only guarantee closedness but also ownership / wrappedness. I like the more explicit version without additional axioms better, though (you may want to add some macro definition to reduce clutter for TLS annotations). HTH, Mark
Jun 16, 2010 at 6:03 PM

Note that something like:

_(axiom \wrapped(o))

will cause soundness issues (because it applies to all threads), so I would second Mark’s opinion.

Michal

Jun 17, 2010 at 10:15 AM

Thanks for this insight, I'll use the version with explicit passing of the TLS data, instead of introducing possibly inconsistent axioms, then.

Thorsten

Jun 18, 2010 at 9:22 AM

I have removed dedicated TLS support from VCC.