11 comments

  • colonCapitalDee176 days ago
    It&#x27;s never actually explained how n=2 is possible. Here&#x27;s how it works:<p>P1 and P2 start executing. P1 sets temp=1, then P2 runs through the loop for i=1..9. Then P1 sets n=temp=1. P2 sets temp=2, then P1 resumes executing for i=2..10, and completes. P2 sets n=temp=2, then completes.<p>The intuition is P1 checkpoints, P2 runs through the loop up until the last iteration, P1 resets n to the checkpoint + 1, P2 checkpoints, P1 runs through the loop, then P2 resets n to the checkpoint + 1.
    • simplegeek175 days ago
      Thank you! I initially included the illustration and explanation in the first draft but decided to remove them in favor of the full trail. Looking back, I think that was a mistake. I’ve now added back the illustration along with some explanation.
  • tombert176 days ago
    This was fun to port over to PlusCal to verify it myself:<p><pre><code> EXTENDS Naturals, Sequences (*--algorithm StateStore { variables n = 0; completions = &lt;&lt;&gt;&gt;; define { Invar == Len(completions) = 2 =&gt; n # 2 } fair process (thing \in {&quot;p&quot;, &quot;q&quot;}) variables i = 0, temp = 0; { Loop: while (i &lt; 10) { First: temp := n + 1; Second: n := temp; Last: i := i + 1; }; Complete: completions := Append(completions, 1) } }*) </code></pre> (I acknowledge that this isn&#x27;t the most elegant Pluscal but I think it is a roughly accurate?)
    • simplegeek176 days ago
      Thank you :) I was wondering how this would look in TLA+&#x2F;PlusCal.
  • Groxx176 days ago
    To be pedantic (which I feel is fair because it&#x27;s a concurrency question about possibilities):<p>&gt;<i>If we run P and Q concurrently, with ‘n’ initialized to zero, what would the value of ‘n’ be when the two processes finish executing their statements?</i><p>It depends a lot on the observer of `n` and what relationship it has with P and Q. Which isn&#x27;t defined.<p>E.g. a trivial boundary-answer is that it can be 0, if nothing guarantees that P&#x27;s and Q&#x27;s threads&#x27; memory reaches the `n`-observer&#x27;s thread. This is somewhat common if you try to synchronize via `sleep`, because that usually doesn&#x27;t guarantee anything as all.<p>We also don&#x27;t know the computer architecture. We can probably assume at least one byte moves between memory levels atomically, because basically every practical system does that, but that doesn&#x27;t have to be true. If <i>bits</i> move between memory levels independently, this could observe <i>31</i>, because it can be any combination of the bits between `00000` and `10100`, which includes `01011` -&gt; there can be a `1` in any position, including all positions, so you can observe a number that was <i>never</i> assigned. (IRL: multi-word values and partial initializations can do this, e.g. it&#x27;s why double-checked locking is flawed without something to guarantee initialization completes before the pointer is exposed)
    • simplegeek176 days ago
      You&#x27;re right, I could have phrased it better to something like:<p>&quot;If we run P and Q concurrently with ‘n’ initialized to zero, what extreme interleaving could result in the lowest value of &#x27;n&#x27; when the two processes finish executing their statements on a model checker?&quot;<p>I&#x27;ll edit it to improve, thanks.
      • Groxx176 days ago
        tbh I think zero is a completely reasonable result for a general thought-exercise like this. sleep-based &quot;memory fixes&quot; are quite common in practice, and there&#x27;s no synchronization at all in the sample.<p>though there&#x27;s a lot of fun in here if you allow for optimizing compilers and lack of synchronization. e.g. without explicit synchronization between P&#x2F;Q and the observing thread (assuming it&#x27;s the main thread), it&#x27;s reasonable for a compiler to simply delete P and Q entirely and replace the whole program with `print(0)`
  • fjfaase179 days ago
    This implicitely assumes atomic assignments, meaning that during an assignment all bits representing a value are transfered in one atomic unit. This sounds a bit trivial, but if one would be working with large integers that are stored in multiple memory words, it is less trivial.<p>I think it is possible to implement locking with only atomic assigments.
    • jprete175 days ago
      I get your point, and my first question was &quot;what operations are even atomic here for this problem to be well-defined?&quot;.<p>But I think &quot;language operations are atomic and everything else isn&#x27;t&quot; is a reasonable inference for a puzzle.<p>I&#x27;m also intrigued by locking being done through atomic assignments; I thought it required at least something like &quot;write if equal to value&quot; or &quot;write new value and return old&quot;.
      • fjfaase175 days ago
        The idea is that there is one task that does the locking. It does so by copying a value from a memory location A to B, when B is equal 0 (the initial value) at regular intervals. Any task that wants to get the lock, writes a unique task identifier (unequal to 0) to memory location A and starts polling B. When it becomes equal to its task identifier, it did get the lock. To release the lock, it writes 0 to B. If it did not get the lock and sees that B has become zero, and A is different, it may overwrite A with its own task identifier.<p>This locking is &#x27;slow&#x27; and has &#x27;unfair&#x27; behavior.
        • fjfaase174 days ago
          I think that the following PROMELA code proofs it:<p><pre><code> byte n = 0 byte A = 0 byte B = 0 proctype Client(byte id) { do :: (A == 0) -&gt; B = id :: (A == id) -&gt; n = n + 1; assert (n &lt;= 1); n = n - 1; A = 0 od } proctype LockServer() { do :: (A == 0) -&gt; A = B od } init { atomic { run LockServer(); run Client(1); run Client(2); run Client(3); } } </code></pre> It fails when two &#x27;Client(2)&#x27; is replaced by &#x27;Client(1)&#x27;
    • yencabulator175 days ago
      You can replace the read and store with atomic operations and n==2 is still possible. As far as I can tell, the model being verified already uses atomic operations.
    • bcoates176 days ago
      Yeah, looking at the code my &#x27;intuition&#x27; was &quot;this is a classic data race, the program is broken&quot; not &quot;somewhere between 10 and 20&quot;.<p>I suppose if you assume all global accesses are atomic, it&#x27;s a good demonstration that atomic operations don’t compose atomically (even in trivial cases) and aren&#x27;t particularly useful as concurrency primitives.
      • Salgat175 days ago
        The question is more testing your full understanding of why this is a race condition, including understanding the possible side effects, since that&#x27;s the only thing you start out with when someone sends in a bug report.
  • hedin_hiervard175 days ago
    I was once asked a very similar problem during a job interview for a position of a software engineer. I was offered to solve it on a piece of paper or orally. We ran out of time and they offered me to take it home. I did and I spent a few hours thinking about it. Google and ChatGPT were not able to produce better results than the intuitive answer, so I built a test program that confirmed the weird behaviour. After meditating for a few hours I was able to find the correct answer and I was indeed fascinated by this. Do you also think it&#x27;s too much for a usual interview?
    • kunley175 days ago
      Kudos for solving this. And yes, this is too much for a job interview.
      • burfle175 days ago
        I don&#x27;t think this an unreasonable puzzle for a role that involves problem-solving or security.<p>You can read the code, figure out what primitives you have, translate the problem into something simple (I like card and board games), then map it back.<p>Problem: two processes each do this ten times: - read the counter - do any number of other things in other processes - write back what you read, plus one.<p>Game: You have two piles of cards. Each card costs 1 move to play, but lets you discard any number of cards from other piles at the same time.<p>Solution: play one red card, discarding everything but one blue card. Play the single remaining blue card, discarding the leftover red cards.<p>Back: process 1 reads, process 2 runs 9 steps, process 1 writes, process 2 reads, process 1 finishes, process 2 writes.
  • sim7c00175 days ago
    the best thing i think i read somewhere is to think of modern cpus as a bunch of computers on a network. each task is transmitted in messages over the network potentially, executed and its result sent back in a packet. despite this not being fully accurate it does give an idea that even in a set of 100 operations, due to caches, latencies and also kernel&#x2F;hardware stuff happening during these 100 operations however much you try to isolate them, the first operation submitted might see its result sent back last.<p>this will help to determine or realize better when and where synchronization is needed even though you might not expect it. (or remoddeling of the code).<p>its extremely hard to writr concurrent code well. i think i&#x27;ve hardly ever managed lockless code that wasnt super bugy (yet! :D). it takes a lot of focus and patience, and tons details about the platform(s) it might run on.
  • chozang174 days ago
    Bonus points for mentioning Spin. My &quot;Software Engineering&quot; course in 1987 in grad school would have been more accurately titled, &quot;Using the Spin Model Checker&quot;. Except when I was looking for it, I had never came across any mention of Spin since.
  • jpc0175 days ago
    As another commentator mentioned, you have violated a precondition, there&#x27;s no point trying to understand what would happen because its indeterminate.
  • Izikiel43176 days ago
    The intuition I developed over the years says that result is unknown, it&#x27;s a race condition, all bets are off. Specially since doing N+1.
  • dtgriscom176 days ago
    Seems pretty clear that the result could be anything from 1 to 20.<p>(Assumes atomic assignments, as noted by someone else.)
    • vbsd176 days ago
      What sort of an interleaving would produce 1? Seems provably impossible to me, assuming atomic assignments.
      • dtgriscom173 days ago
        I took another look, and AFAICT you&#x27;re right. The best I can do is get the value 2:<p>* Run procedure P into its first iteration, stopping after temp is assigned &quot;n + 1&quot;, or the value 1<p>* Run procedure Q through nine iterations, stopping after the ninth has completed (n changes, but who cares?)<p>* Run the next line of procedure P&#x27;s first iteration, so that it assigns temp&#x27;s value of 1 to n; n is now 1<p>* Run procedure Q into its tenth iteration, stopping after temp is assigned the value 2<p>* Complete procedure P (n changes, but who cares?)<p>* Complete procedure Q, so that n is assigned the value of temp, or 2.
  • lincpa176 days ago
    [dead]