{
  "$type": "site.standard.document",
  "bskyPostRef": {
    "cid": "bafyreifgki2epj6pjsi5pk5vt2ulhkhoj6duvks5ody6s5fohz73y5qf34",
    "uri": "at://did:plc:46ti67tc37qcmwp2vaynk6fq/app.bsky.feed.post/3mo4czlaxdgs2"
  },
  "path": "/2026/06/12/sel4-clock-magic/",
  "publishedAt": "2026-06-12T18:00:04.621Z",
  "site": "https://retout.co.uk",
  "tags": [
    "a small\npatch",
    "issue\n#1352",
    "PR\n#1435",
    "issue #1509"
  ],
  "textContent": "I have been looking at seL4 some more recently, and had a small\npatch merged today to remove a legacy Python module from a helper script. (I was trying to run the script on a system without that module installed, and it was almost easier to patch it out.)\n\nHowever, the more I think about this code and how it’s used, the more it seems wrong on at least five other levels.\n\nThe patch itself is quite uninteresting; this script was importing the `past` module (part of `future`?) to use the `xrange` function. Python 2 used to have separate `xrange` and `range` functions, where `range` returned a list in memory while `xrange` generated an iterator. Because this seL4 script is iterating over a large range of values, it’s important the list is not generated in-memory. But Python 3 removed the `xrange` function and just has `range` return an object, so it’s trivial to avoid the module import.\n\nHaving thought carefully some more about the specific line, there’s surely an off-by-one error in it - `range` iterates over 0 to n-1, so this line shouldn’t be subtracting one if it’s looking to test all 32-bit values:\n\n\n        for i in range(2**32-1):\n\n\nBut then again, this is being used for a ‘sanity check’ of a magic bit shift algorithm that speeds up division operations to convert CPU ticks to microseconds on 32-bit arm platforms. Surely if the algorithm’s good, it shouldn’t be necessary to validate it exhaustively against every possible 32-bit value?\n\nAlso, 32 bits isn’t enough, because this is 64-bit division. `include/api/types.h` shows that `ticks_t` is always a `uint64_t`, so if this were a proof by exhaustion it should run to 2**64 (though that would take infeasibly long).\n\nAs discussed in issue\n#1352, lots of people have been running this code with the wrong divisor anyway. But because the bit shift path is only used on 32-bit platforms, it’s not clear to me that there’s even any point in specifying CLK_SHIFT/MAGIC on platforms which are 64-bit only (e.g. the tx2 port).\n\nAnd to follow this rabbit hole to the very end, in comments on PR\n#1435 and issue #1509 it’s clear that the future of this code is to remove it, as it’s 1. unnecessarily clever (on 64-bit platforms the equivalent code just uses a division, so performance can’t be that important), and 2. the entire concept of converting to microseconds breaks the seL4 principle of not abstracting away details of the hardware.\n\nSo this has left me unclear on whether my small patch was a good thing or not, but I certainly learnt something about this corner of seL4 timer handling. And I’ve ordered a copy of “Hacker’s Delight” on the recommendation of a code comment.",
  "title": "Tim Retout: seL4 clock magic",
  "updatedAt": "2026-06-12T16:45:40.000Z"
}