Using __VERIFIER_spin_{start,end}

[mpi-sws]

Using __VERIFIER_spin_{start,end}

[michaliskok]

Good point regarding __VERIFIER_spin_end. This was due to a merge error, I will push a fix in the next release. (I was actually debating whether these should be exposed to users; if you think they would be useful, I will also clean up the interface a bit and add some documentation.)

1. __VERIFIER_spin_start should not have been included in that header. In some previous (tentative) version it was used similarly to the way it is used in your example, but in the current one it is inserted automatically by GenMC when liveness checks are specified or when some other dynamic checks are necessary.

__VERIFIER_spin_end is also inserted automatically, but you could manually insert it at a loop latch, as long as all paths from the header to the latch are side-effect-free. It takes as an argument a condition that, if false, will block the execution of the loop.

2. Yes
3. Yes
4. As long as these loops correspond to LLVM-IR loops, yes.

That said, I would be interested in seeing examples where GenMC fails to automatically transforms spinloops with side-effects (like #15). If you are aware of any others, please let me know.

[JonasOberhauser]

Good point regarding __VERIFIER_spin_end. This was due to a merge error, I will push a fix in the next release. (I was actually debating whether these should be exposed to users; if you think they would be useful, I will also clean up the interface a bit and add some documentation.)

They're definitely sometimes necessary for "advanced users" , when the automation doesn't catch the loop. We have several such examples right now and I'll check if we can forward them to you.

I don't know if it's worth putting too much effort into documenting these functions, since the set of advanced users who can use this correctly is pretty much limited to the people who already know what it does, and I don't see that changing by any amount of documentation. I think two or three example test cases should suffice together with a link in the manual.

I think it's more useful having very good documentation of the part of GenMC that automatically transforms loops into this, so that people can extend that if necessary.

[db7]

Thanks for the reply. It looks promising.

I think these could be very useful to be exposed. I imagine that automatic detection can be tricky sometimes. For some applications, it could be useful to disable automatic detection (how to do that?) and only use the manual instrumentation.

So, for my simple example, the following would be ok.

while (atomic_load(&me->next) == NULL) {
   // nothing (side-effect free)
   __VERIFIER_spin_end(0);
}

Removing spin_start() and spin_end(1). Or will this have a gap between the check of next and the decision of blocking?

If I find more examples like #15, I'll let you know. Thanks.

[michaliskok]

I think these could be very useful to be exposed. I imagine that automatic detection can be tricky sometimes. For some applications, it could be useful to disable automatic detection (how to do that?) and only use the manual instrumentation.

Using -disable-spin-assume will disable automatic spinloop transformation.

So, for my simple example, the following would be ok.

while (atomic_load(&me->next) == NULL) {
   // nothing (side-effect free)
   __VERIFIER_spin_end(0);
}

Removing spin_start() and spin_end(1). Or will this have a gap between the check of next and the decision of blocking?

The above code looks OK for this example. I am not exactly sure what you mean by a "gap"; it can be the case that after reading next the tool executes some more LLVM-IR instructions (until it reaches the __VERIFIER_spin_end()), but it will never execute the loop header again (in that execution).

[db7]

Using -disable-spin-assume will disable automatic spinloop transformation.

Nice, but I had to manually add __VERIFIER_spin_start() to make -check-liveness work with -disable-spin-assume.

The above code looks OK for this example. I am not exactly sure what you mean by a "gap"; it can be the case that after reading next the tool executes some more LLVM-IR instructions (until it reaches the __VERIFIER_spin_end()), but it will never execute the loop header again (in that execution).

Ok, thank you.

[michaliskok]

Using -disable-spin-assume will disable automatic spinloop transformation.

Nice, but I had to manually add __VERIFIER_spin_start() to make -check-liveness work with -disable-spin-assume.

Yes, sorry, I forgot to mention that about liveness checks. If you are not using __VERIFIER_spin_end() on top of the automatic transformations, make sure to add __VERIFIER_spin_start() at the beginning of the loop header, right after all Φ nodes. (It marks the beginning of an iteration.) This might be easier to do if you are directly manipulating the LLVM-IR.

[db7]

Just to be sure I understood how to use this properly, assuming we can't manipulate the LLVM-IR, would the following be sufficient?

do {
      __VERIFIER_spin_start();  // start iteration
      // side-effect-free body
      if (cond) {
          __VERIFIER_spin_end(1);
          break;
      } else __VERIFIER_spin_end(0);
} while (1);

Or perhaps this more generic version:

for (int tmp = (__VERIFIER_spin_start(), 0);  // start() marks first iteration
      tmp = cond, __VERIFIER_spin_end(!tmp), tmp;  // tell GenMC if loop will break or not.
      __VERIFIER_spin_start()) // start() marks second and subsequent iterations
{
   // side-effect-free body
}

[michaliskok]

The first one looks OK. You can also skip the __VERIFIER_spin_end(1); statement, as it is OK for a latch to not have a __VERIFIER_spin_end().

The second one is wrong. Instead, I would recommend the following:

for (int tmp = 0; __VERIFIER_spin_start(), tmp = cond, __VERIFIER_spin_end(!tmp), tmp; /* nothing here */) {
    /* statements here will be ignored */
}

In the one above, the __VERIFIER_spin_start() is not in the loop initialization block (the statements of which should not be taken into account when doing, e.g., liveness checks), but rather in the beginning of the loop header. Of course, in loops like this one, the statements of the body will not be executed as either the loop will be terminated by __VERIFIER_spin_end(), or the condition will be false and the body will be skipped.

[db7]

Thanks, these comments were very helpful.

The body of such loops typically have something like asm ("pause");, so it should be fine.

[michaliskok]

Documented in v0.6.1 in genmc.h. A __VERIFIER_loop_begin() statement is also required if these markers are used along with spin-assume. (If spin-assume is disabled not using __VERIFIER_loop_begin() should be OK.)