sddf queue functional correctness

[midnightveil]

I am concerned about the functional correctness of the queue under multicore.

My mental model to the i2c_queue_handle_t queue is that,

1. the producer core performs a number of calls to i2c_enqueue_request
2. the producer core calls i2c_request_commit
3. the consumer core calls i2c_dequeue_request

I make an abstraction of the execution as follows (the idea is that the producer writes to data, and then writes to flag; if the consumer observes the change to flag, it should read the new data. I upgrade all memory operations to relaxed atomics to ignore the data race issue in the original code)

link

Running the code snippet with GenMC v0.13.0 gives the following result

link

This shows that the consumer may read the stale value ((2, 2): Rrlx (data, 0) [INIT] L.36) instead, which violates the functional correctness.

---

Another question is, should we provide different implementations for single-core and SMP microkit?

Originally posted by @KurtWu10 in https://github.com/au-ts/sddf/issues/509#issuecomment-3351632634

Then, from me:

@KurtWu10 This perhaps best should be discussed in person, but your model seems no different to that of our existing sDDF queues (i.e. it's not specific to this i2c queue); your model just has a data and flag which isn't special for i2c, as most of our other queues are precisely the same as this.

Feel free to pull this out into another issue (fwiw I'd love to see some kind of model checking run automatically like this in-repo as CI).

Personally I'm not quite sure where the issue is; is the issue that we use a release and not an acquire in the consumer?

Then, from Kurt:

@midnightveil Yes, I just wanted to make a simple note here, using an (overly) simplified implementation as an example. I would like to discuss my understanding in detail in person.

The issue of my code is that there should be an acquire fence between the two reads in the consumer. The original code has other issues, including the release fence issue.

[gernotheiser]

Another question is, should we provide different implementations for single-core and SMP microkit?

Simple answer: no.

The world is multicore and I haven't seen a use case where people really only want to use a single core. Location transparency of sDDF/LionsOS components is an important feature.

So I don't see the point of a single-core Microkit version, its only use would be for (misleading) benchmarking

[midnightveil]

From discussing this further in person:

• There was an I²C specific issue where we had a THREAD_MEMORY_RELEASE in the wrong spot, the other queues are fine.

• Kurt has other concerns where our queues (ab)use the C memory model THREAD_MEMORY_RELEASE being compiled into a (stronger) memory barrier at the ARM memory model level; so assuming a sufficiently dumb compiler the queues are correct at a hardware level. (A sufficiently clever compiler could in theory notice the lack of an acquire and miscompile this).

[KurtWu10]

To show the issue of our use of THREAD_MEMORY_RELEASE for the consumer on risc-v, consider this test, where it is desired that once the consumer observes the updated flag, it should also observe the updated data.

I manually translate the risc-v assembly into a litmus test, and run it with herd7 7.58. The result shows that the consumer can observe the stale data.

This should be solved by using THREAD_MEMORY_ACQUIRE in the consumer. This can benefit performance on aarch64 as well with the use of dmb ishld load fence instead of the dmb ish full fence.

This is my current progress in fixing the existing code. From an in-person discussion with Ivan, it is desired that spsc queue implementations in sddf should follow the implementation in lionsos/fs. I will update the implementation in a new sddf branch properly later.