Thank you for that write-up! Sorry that my response is so slow. (Seems I can still reply several days later, wonder what the limit actually is) That's definite

Thank you for that write-up! Sorry that my response is so slow. (Seems I can still reply several days later, wonder what the limit actually is) That's definitely both a nice solution to the problem, and I found it pretty enlightening (having sadly not used anything as strongly typed as Haskell). In the case of global variables, if performance didn't matter then it would be possible to just pass around a pointer to a struct of the thread-local/thread-locked data for use directly. I spent a while trying to come up with some alternatives or generalisation of your approach, and found it was really hard to match the same guarantees without a run-time cost. One idea I got from your description is putting access to certain data/function in scope in a type-checked way. So you could put multiple such contexts (pointers or other access methods like functions or even macros) in scope at the top of the function/block, rather than having to type-check every access throughout the function using an implicit control (e.g. the 'th' variable.) But really, that's just equivalent to using the L macro like so: void inc_foo(video_thread_t th) { video_thread_data_t *vid = &L(video_data); // checked global access vid->foo++; vid->bar++; } I think something like this looks more natural though.