DblPlusUngood

Yes.

In some cases, yes (if there are other runnable threads on this CPU's queue).

A better example: a page fault for a non-present page.

Don't forget gltron!

You are absolutely right. They are used everywhere in the Linux, OpenBSD, and FreeBSD kernels, and likely many other kernels.

Replacing large linked lists with arrays is rarely an actual win. With an array, insertion and deletion become far more expensive, virtual memory is more likely to become fragmented or grow monotonically, and the cache misses avoided are almost certainly irrelevant to total performance.

> I don't see how it could. Kernel data structures don't go on pagecache pages.

Kernel data structures could end up on a pagecache page: all it takes is a reference counting bug and the page could be reallocated in the kernel heap, which is directly mapped by user space. Keeping user-mapped pages and pagecache pages distinct makes this less likely.

I am otherwise not convinced that there is an actual problem with OpenBSD's coherency plan.

OpenBSD's choice is arguably reasonable, given their prioritization of security, since it reduces opportunities for user programs to corrupt kernel memory.

What is the problem with OpenBSD's plan for coherency? Why is the burden of explicitly calling msync(2) too much?

What coherence is lacking? OpenBSD supports msync(2), which is the only POSIX mechanism I know of for ensuring coherency between read(2) and shared file mappings. Otherwise relying on unspecified behavior sounds dangerous.

Is recovery of a shared memory queue after one of the workers crashes even possible, in general? (what if the worker crashed before releasing a lock?)

Sounds like a fun project!

Isn't seL4's multicore support either unverified or limited (i.e. shared memory is forbidden)? Is your platform single-threaded then?

Yes. In theory, maybe it's useful to have more flexibility to trade-off durability for performance (smaller quorum size hopefully reduces deciding latency [unless your small quorum contains the straggler!]) for specific kinds of data in the same replica group.

In practice though, it seems easier just to run separate instances of Paxos.

Instead of an ad hominem, please clearly explain the main way that the example Go code is less safe than the C example code.

This is a great point. Jargon can be really intimidating and make the simplest statements impossible to understand for the unfamiliar. But is often trivial to learn with a little study.