Strange timing results?

Stream: lean4

[James Gallicchio]

I've been trying to time different operations with IO.monoMsNow which seemed to be working great, until I wrote up this test case:

def test3 (iters len : Nat) (α) [Q : Queue α Nat] : IO Int := do
  let (t_no_deq,()) ← time (
    for _ in [:iters] do
      let mut q := Q.empty
      for i in [:len] do
        q := Q.enq q i
  )

  let (t_deq,()) ← time (
    for _ in [:iters] do
      let mut q := Q.empty
      for i in [:len] do
        q := Q.enq q i
      match Q.deq q with
      | none => IO.println "early empty??"
      | some (x,_) =>
        if x ≠ 0 then
          IO.println "wrong entry??"
  )

  pure ((Int.ofNat t_deq) - t_no_deq)

In both loops, this code pushes len elements onto a queue. In the second loop it also removes the first element of the queue.

Weirdly, in one of my implementations, the second loop consistently runs faster than the first. Even if I switch the order of the two blocks, it still runs faster when doing a deq than without. Any idea why?

The full code is here:
https://github.com/JamesGallicchio/LeanColls/blob/master/LeanColls/Queue/Main.lean

[James Gallicchio]

time is just doing the obvious thing:

def time (f : IO α) : IO (Nat × α) := do
  let pre ← IO.monoMsNow
  let ret ← f
  let post ← IO.monoMsNow
  pure (post-pre, ret)

[Jannis Limperg]

Can't reproduce; I'm getting +200ms difference for the test3 in your repo with 1000 iterations, 100000 elements and BQueue Nat. Could you make a branch of your repo where testAll is the exact test case you're referring to?

In general, you shouldn't be able to measure any difference here since the dequeue operation hopefully takes less than 1ms.

[James Gallicchio]

Hm, today I can't reproduce it. It must have been a fluke; it only occurred with RTQueue on relatively small element counts.

I was repeating the test for that many iterations in order to be able to measure the difference of a single dequeue (1000 dequeues should be measurable, even if 1 isn't). But evidently the timing is too noisy. I'm gonna see if I can reduce the noise and get better results.