I'm looking at the makeTVal code:<div><span style="font-family:'times new roman';font-size:16px"><pre><span style="color:blue"><span style="font-size:small">data</span></span><span style="font-size:small"> </span><span><span style="font-size:small">TVal</span></span><span style="font-size:small"> </span><span><span style="font-size:small">t</span></span><span style="font-size:small"> </span><span><span style="font-size:small">a</span></span><span style="font-size:small"> </span><span style="color:red"><span style="font-size:small">=</span></span><span style="font-size:small"> </span><span><span style="font-size:small">TVal</span></span><span style="font-size:small"> </span><span style="color:red"><span style="font-size:small">{</span></span><span style="font-size:small"> </span><span><span style="font-size:small">timeVal</span></span><span style="font-size:small"> </span><span style="color:red"><span style="font-size:small">::</span></span><span style="font-size:small"> </span><span style="color:red"><span style="font-size:small">(</span></span><span><span style="font-size:small">t</span></span><span style="color:red"><span style="font-size:small">,</span></span><span><span style="font-size:small">a</span></span><span style="color:red"><span style="font-size:small">)</span></span><span style="color:red"><span style="font-size:small">,</span></span><span style="font-size:small"> </span><span><span style="font-size:small">definedAt</span></span><span style="font-size:small"> </span><span style="color:red"><span style="font-size:small">::</span></span><span style="font-size:small"> </span><span><span style="font-size:small">t</span></span><span style="font-size:small"> </span><span style="color:red"><span style="font-size:small">-></span></span><span style="font-size:small"> </span><span><span style="font-size:small">Bool</span></span><span style="font-size:small"> </span><span style="color:red"><span style="font-size:small">}</span></span><span style="font-size:small">
</span><span><span style="font-size:small">makeTVal</span></span><span style="font-size:small"> </span><span style="color:red"><span style="font-size:small">::</span></span><span style="font-size:small"> </span><span><span style="font-size:small">Clock</span></span><span style="font-size:small"> </span><span><span style="font-size:small">TimeT</span></span><span style="font-size:small"> </span><span style="color:red"><span style="font-size:small">-></span></span><span style="font-size:small"> </span><span><span style="font-size:small">MkFed</span></span><span style="font-size:small"> </span><span style="color:red"><span style="font-size:small">(</span></span><span><span style="font-size:small">TVal</span></span><span style="font-size:small"> </span><span><span style="font-size:small">TimeT</span></span><span style="font-size:small"> </span><span><span style="font-size:small">a</span></span><span style="color:red"><span style="font-size:small">)</span></span><span style="font-size:small"> </span><span><span style="font-size:small">a</span></span><span style="font-size:small">
</span><span><span style="font-size:small">makeTVal</span></span><span style="font-size:small"> </span><span style="color:red"><span style="font-size:small">(</span></span><span><span style="font-size:small">Clock</span></span><span style="font-size:small"> </span><span><span style="font-size:small">getT</span></span><span style="font-size:small"> </span><span style="color:blue"><span style="font-size:small">_</span></span><span style="color:red"><span style="font-size:small">)</span></span><span style="font-size:small"> </span><span style="color:red"><span style="font-size:small">=</span></span><span style="font-size:small"> </span><span><span style="font-size:small">f</span></span><span style="font-size:small"> </span><span><span style="font-size:small"><$></span></span><span style="font-size:small"> </span><span><span style="font-size:small">newEmptyIVar</span></span><span style="font-size:small">
</span><span style="color:blue"><span style="font-size:small">where</span></span><span style="font-size:small">
</span><span><span style="font-size:small">f</span></span><span style="font-size:small"> </span><span><span style="font-size:small">v</span></span><span style="font-size:small"> </span><span style="color:red"><span style="font-size:small">=</span></span><span style="font-size:small"> </span><span style="color:red"><span style="font-size:small">(</span></span><span><span style="font-size:small">TVal</span></span><span style="font-size:small"> </span><span style="color:red"><span style="font-size:small">(</span></span><span><span style="font-size:small">readIVar</span></span><span style="font-size:small"> </span><span><span style="font-size:small">v</span></span><span style="color:red"><span style="font-size:small">)</span></span><span style="font-size:small"> </span><span style="color:red"><span style="font-size:small">(</span></span><span><span style="font-size:small">unsafePerformIO</span></span><span style="font-size:small"> </span><span><span style="font-size:small">.</span></span><span style="font-size:small"> </span><span><span style="font-size:small">undefAt</span></span><span style="color:red"><span style="font-size:small">)</span></span><span style="color:red"><span style="font-size:small">,</span></span><span style="font-size:small"> </span><span><span style="font-size:small">sink</span></span><span style="color:red"><span style="font-size:small">)</span></span><span style="font-size:small">
</span><span style="color:blue"><span style="font-size:small">where</span></span><span style="font-size:small">
</span><span><span style="font-size:small">undefAt</span></span><span style="font-size:small"> </span><span><span style="font-size:small">t</span></span><span style="font-size:small"> </span><span style="color:red"><span style="font-size:small">=</span></span><span style="font-size:small">
</span><span style="color:green"><span style="font-size:small">-- Read v after time t. If it's undefined, then it wasn't defined</span></span><span style="font-size:small">
</span><span style="color:green"><span style="font-size:small">-- at t. If it is defined, then see whether it was defined before t.</span></span><span style="font-size:small">
</span><span style="color:blue"><span style="font-size:small">do</span></span><span style="font-size:small"> </span><span style="color:green"><span style="font-size:small">-- ser $ putStrLn $ "sleepPast " ++ show t</span></span><span style="font-size:small">
</span><span><span style="font-size:small">sleepPast</span></span><span style="font-size:small"> </span><span><span style="font-size:small">getT</span></span><span style="font-size:small"> </span><span><span style="font-size:small">t</span></span><span style="font-size:small">
</span><span style="color:green"><span style="font-size:small">-- maybe True ((> t) . fst) <$> tryReadIVar v</span></span><span style="font-size:small">
</span><span><span style="font-size:small">value</span></span><span style="font-size:small"> </span><span style="color:red"><span style="font-size:small"><-</span></span><span style="font-size:small"> </span><span><span style="font-size:small">tryReadIVar</span></span><span style="font-size:small"> </span><span><span style="font-size:small">v</span></span><span style="font-size:small">
</span><span style="color:blue"><span style="font-size:small">case</span></span><span style="font-size:small"> </span><span><span style="font-size:small">value</span></span><span style="font-size:small"> </span><span style="color:blue"><span style="font-size:small">of</span></span><span style="font-size:small">
</span><span style="color:green"><span style="font-size:small">-- We're past t, if it's not defined now, it wasn't at t.</span></span><span style="font-size:small">
</span><span><span style="font-size:small">Nothing</span></span><span style="font-size:small"> </span><span style="color:red"><span style="font-size:small">-></span></span><span style="font-size:small"> </span><span><span style="font-size:small">return</span></span><span style="font-size:small"> </span><span><span style="font-size:small">False</span></span><span style="font-size:small">
</span><span style="color:green"><span style="font-size:small">-- If it became defined before t, then it's defined now.</span></span><span style="font-size:small">
</span><span><span style="font-size:small">Just</span></span><span style="font-size:small"> </span><span style="color:red"><span style="font-size:small">(</span></span><span><span style="font-size:small">t'</span></span><span style="color:red"><span style="font-size:small">,</span></span><span style="color:blue"><span style="font-size:small">_</span></span><span style="color:red"><span style="font-size:small">)</span></span><span style="font-size:small"> </span><span style="color:red"><span style="font-size:small">-></span></span><span style="font-size:small"> </span><span><span style="font-size:small">return</span></span><span style="font-size:small"> </span><span style="color:red"><span style="font-size:small">(</span></span><span><span style="font-size:small">t'</span></span><span style="font-size:small"> </span><span><span style="font-size:small"><</span></span><span style="font-size:small"> </span><span><span style="font-size:small">t</span></span><span style="color:red"><span style="font-size:small">)</span></span><span style="font-size:small">
</span><span><span style="font-size:small">sink</span></span><span style="font-size:small"> </span><span><span style="font-size:small">a</span></span><span style="font-size:small"> </span><span style="color:red"><span style="font-size:small">=</span></span><span style="font-size:small"> </span><span style="color:blue"><span style="font-size:small">do</span></span><span style="font-size:small"> </span><span><span style="font-size:small">t</span></span><span style="font-size:small"> </span><span style="color:red"><span style="font-size:small"><-</span></span><span style="font-size:small"> </span><span><span style="font-size:small">getT</span></span><span style="font-size:small">
</span><span><span style="font-size:small">writeIVar</span></span><span style="font-size:small"> </span><span><span style="font-size:small">v</span></span><span style="font-size:small"> </span><span style="color:red"><span style="font-size:small">(</span></span><span><span style="font-size:small">t</span></span><span style="color:red"><span style="font-size:small">,</span></span><span><span style="font-size:small">a</span></span><span style="color:red"><span style="font-size:small">)</span></span></pre>
<pre><span class="Apple-style-span" style="font-family: arial; font-size: 13px; white-space: normal; ">I assume the sink function is called from a different thread than the one on which undefAt is called.</span><br></pre>
<pre><span class="Apple-style-span" style="font-family: arial; font-size: 13px; white-space: normal;">Suppose a thread switch happens just before the (t,a) value is written to the IVar in</span></pre><pre><span style="font-size: small; "> </span><span><span style="font-size: small; ">sink</span></span><span style="font-size: small; "> </span><span><span style="font-size: small; ">a</span></span><span style="font-size: small; "> </span><span style="color: red; "><span style="font-size: small; ">=</span></span><span style="font-size: small; "> </span><span style="color: blue; "><span style="font-size: small; ">do</span></span><span style="font-size: small; "> </span><span><span style="font-size: small; ">t</span></span><span style="font-size: small; "> </span><span style="color: red; "><span style="font-size: small; "><-</span></span><span style="font-size: small; "> </span><span><span style="font-size: small; ">getT</span></span><span style="font-size: small; ">
</span><span><span style="font-size: small; ">writeIVar</span></span><span style="font-size: small; "> </span><span><span style="font-size: small; ">v</span></span><span style="font-size: small; "> </span><span style="color: red; "><span style="font-size: small; ">(</span></span><span><span style="font-size: small; ">t</span></span><span style="color: red; "><span style="font-size: small; ">,</span></span><span><span style="font-size: small; ">a</span></span><span style="color: red; "><span style="font-size: small; ">)</span></span></pre>
<pre><span class="Apple-style-span" style="font-family: arial; font-size: 13px; white-space: normal;">Lets call the t above t1. </span></pre><pre><span class="Apple-style-span" style="font-family: arial; font-size: 13px; white-space: normal; ">Now sleepPast getT t is evaluated on the other thread. </span></pre>
<pre><span class="Apple-style-span" style="font-family: arial; font-size: 13px; white-space: normal;"><span class="Apple-style-span" style="font-family: 'times new roman'; font-size: 16px; "><pre><span style="font-size: small; "> </span><span><span style="font-size: small; ">sleepPast</span></span><span style="font-size: small; "> </span><span><span style="font-size: small; ">getT</span></span><span style="font-size: small; "> </span><span><span style="font-size: small; ">t</span></span><br>
</pre><div><span class="Apple-style-span" style="font-family: arial; font-size: 13px; ">Assume the parameter t passed to sleepPast is really close to t1 but larger than t1. Call it t2. So t1 < t2.</span></div><div><span class="Apple-style-span" style="font-family: arial; font-size: 13px;"><br>
</span></div><div><span class="Apple-style-span" style="font-family: arial; font-size: 13px; ">Call t3 the time as evaluated by getT in the sleepPast function. So t1 < t2 < t3 (since t3 is read a after t1, and since the clock is serialized, this is the case I guess)</span><br>
</div><div><span class="Apple-style-span" style="font-family: arial; font-size: 13px; ">Since t3 > t2, sleepPast will not call threadDelay, so it is not unlikely that a thread switch happens. But then </span><br></div>
</span></span></pre><pre><span class="Apple-style-span" style="font-family: arial; font-size: 13px; white-space: normal;"><span class="Apple-style-span" style="font-family: 'times new roman'; font-size: 16px; "><pre>
<span style="font-size: small; "> </span><span><span style="font-size: small; ">value</span></span><span style="font-size: small; "> </span><span style="color: red; "><span style="font-size: small; "><-</span></span><span style="font-size: small; "> </span><span><span style="font-size: small; ">tryReadIVar</span></span><span style="font-size: small; "> </span><span><span style="font-size: small; ">v</span></span></pre>
<pre><span class="Apple-style-span" style="font-size: 12px;"><span class="Apple-style-span" style="font-family: 'times new roman'; font-size: 16px; white-space: normal; "><pre><span class="Apple-style-span" style="font-family: arial; font-size: 13px; white-space: normal; ">evaluates to Nothing, since the IVar is not written to yet. So <span class="Apple-style-span" style="font-family: -webkit-monospace; font-size: 12px; white-space: pre; ">undefAt </span><span class="Apple-style-span" style="font-size: 12px; white-space: pre; "><span class="Apple-style-span" style="font-family: arial, helvetica, sans-serif;">will return False, although clearly t1 < t2 and so it should have returned True.</span></span></span></pre>
<pre><span class="Apple-style-span" style="font-family: arial; font-size: 13px; white-space: normal;">I'm not sure if my reasoning is correct. But if it is, it would be solvable my making sure that getting the time from clock and writing it to the IVar is an atomic operation.</span></pre>
<pre><span class="Apple-style-span" style="font-family: arial; font-size: 13px; white-space: normal;">Does any of the above make sense?</span></pre><pre><span class="Apple-style-span" style="font-family: arial; font-size: 13px; white-space: normal;"><br>
</span></pre><pre><span class="Apple-style-span" style="font-family: arial; font-size: 13px; white-space: normal;"><br></span></pre><pre><span class="Apple-style-span" style="font-family: arial; font-size: 13px; white-space: normal;"><br>
</span></pre></span></span></pre></span></span></pre><pre><span class="Apple-style-span" style="font-family: arial; font-size: 13px; white-space: normal;"><br></span></pre></span></div>