Re: [tlaplus] Novel queue-lock like concurrent spin-lock formalization in TLA+

On Saturday, June 24, 2017 at 5:50:17 PM UTC+1 Stephan Merz wrote:

Hi Steven,

sorry for replying so late: I had a look at your PlusCal model of the algorithm, and I think that it is very competently written. (I have not tried to understand the algorithm, though.)

A (standard) suggestion for mitigating state space explosion is to reduce labels as much as you can, and of course as far as it doesn't impact the verdict of model checking. For example, I noticed some patterns like the following:

  if Acquired then
RET: return;
end if;
UPDATE_COUNTER:
Counter := Counter + 1;

and I believe that the only reason for having label UPDATE_COUNTER is syntactic, since PlusCal needs a label at the statement following a conditional statement. However, you can rewrite your code to the semantically equivalent

  if Acquired then
RET: return;
  else
Counter := Counter + 1;
end if;

and save a label. This is relevant because TLC will non-deterministically schedule any executable thread at every label.

Of course, state explosion will set in despite these changes, and then you should think about how many threads you would like to check in order to be reasonably confident about correctness.

Best regards,
Stephan

On 16 Jun 2017, at 02:12, Steven Stewart-Gallus <stevensele...@xxxxxxxxx> wrote:

See https://sstewartgallus.com/git?p=qlock.git;a=blob;f=tla/StackLock.tla;h=6884d808b5ffd605e912f4b12ae38928fd9b8313;hb=HEAD for the code.

On many-core machines spin locks can be slow because the cores ping each other constantly. To improve on this people often use test-and-test and set locks as loads from a memory location are often cheaper than exchange and compare and exchange operations. However, there is still a small amount of intercore communication which can be expensive on machines with a whole lot of cores. To improve on this the MCS and CLH queue locks were invented. Basically, in these algorithms each waiting core spins on its own separate memory location which is linked into a queue. This may possibly be faster in some scenarios although for little-core machines the added complexity is often slower. A deficiency with these algorithms is that the waiters are ordered in strict FIFO queue order and no other scheme is possible. For example, one might want to use a priority queue (for hard real-time scenarios) or a stack (for better raw performance.) I came up with an algorithm (which I think is new but might possibly not be as I am not really an expert on this topic) that allows the ADT details to be easily replaced by any structure that offers push, pop and isEmpty functions. This algorithm can then be used with stacks or priority queues.

I implemented this algorithm in Rust (with the specific case of a stack) and then formalized the abstract details in TLA+ which led to me discovering and fixing a deadlock bug. So far, I have run and tested the model under a number of threads but past 4 or so threads the model checker becomes very slow. Future steps should involve checking to see if more properties can be asserted and tested under the model, scaling the analysis to a larger number of threads, possibly formalizing an abstract proof of correctness for any number of threads and to experimentally validate and check an operation log of the implementation for linearizability with a checker such as Knossos.

Does my TLA+ code look correct? Can anyone any further steps I should take? Does anyone have any other thoughts?

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@xxxxxxxxxxxxxxxx.
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.