Add concurrency checking based on GenMC - serial queue

[KurtWu10]

• This PR is a variant of PR Add concurrency checking based on GenMC #523 that targets serial queues. It should also fix issue serial example failures on Rasberry Pi 4B #528.

• The following invalid assertion

  sddf/include/sddf/serial/queue.h

  Lines 159 to 172 in 63ac0fd

  	/**
  	* Update the value of the tail in the shared data structure to make
  	* locally enqueued data visible.
  	*
  	* @param queue_handle queue to update.
  	* @param local_tail tail which points to the last character enqueued.
  	*/
  	static inline void serial_update_shared_tail(serial_queue_handle_t *queue_handle, uint32_t local_tail)
  	{
  	uint32_t current_length = serial_queue_length(queue_handle);
  	uint32_t new_length = local_tail - queue_handle->queue->head;
  	/* Ensure updates to tail don't overwrite existing data */
  	assert(new_length >= current_length);

  in L172 has also been removed. It is invalid because the consumer can consume multiple queue entries and update the head between L168 and L169.

  A similar assertion in serial_update_shared_head() has also been removed.

• Queue operations with the _length suffix always use relaxed atomic operation to prevent data races in all situations. These operation do not provide any synchronisation. On the contrary, other operations with _empty / _full / _free suffix use acquire atomic operation appropriately for synchronisation.

Limitations

• On the memory model side, compared with PR Add concurrency checking based on GenMC #523, this PR uses additional relaxed atomic operations that may be a concern for verifiers like GenMC.

• The test does not cover all serial queue APIs.

• There are some redundant memory operations that will not be removed in compiler's dead-code elimination optimisation, e.g. in the updated serial_update_shared_tail().

[Courtney3141]

I'm going to make some additional modifications to the serial queue, but otherwise this is a great PR!

[Courtney3141]

Also, I will leave it to you to add the additional comments to all the queue functions:

"This function is only to be called by the CONSUMER/PRODUCER of the queue."

(I'll leave the phrasing up to you)

[Courtney3141]

Also, I will leave it to you to add the additional comments to all the queue functions:

"This function is only to be called by the CONSUMER/PRODUCER of the queue."

(I'll leave the phrasing up to you)

Never mind, I did this in my last commit. Please just check that my comments are in fact correct!

[midnightveil]

Is it really worth having this?

I'd thought we'd discussed this with Gernot and decided the queues should just always be correct for cross-core since it's misleading if not.

(and when I tested it made no performance impact).

[KurtWu10]

I remember the discussion on GitHub as well. I'll run additional benchmarks on this. The current implementation is based on memory of my recent benchmarks that it increases utilisation by 5~10%.

In addition, I will also benchmark whether the dmb ishst barrier is beneficial to the store-release function, which cannot be represented by the C standard library.

[Courtney3141]

I am very surprised by you finding it had no performance impact, as when I tested it a long ago I remember it being very significant. Although I can't seem to find those results for the life of me...

[Courtney3141]

I finally found the graph!

[Courtney3141]

[midnightveil]

I suspect it probably depends on what system we test on, as they will have different costs? But yeah, IDK. All my tests were run with it forced to 1 as per the docs I had in the description.

[KurtWu10]

Yes, it is system dependent. There is an about 5-10% system-wide relative overhead on maaxboard (cortex-a53)

with higher cycles per packet as well. There is no overhead on odroid c4 (cortex-a55, under investigation). These are unicore UDP benchmarks comparing different implementations of network queues.

[Courtney3141]

I'm thinking it may be worth adding an introductory comment at the top of the serial queue file saying something along the lines of:

The serial queue, like all sDDF queues, is an implementation of a single-producer, single-consumer FIFO queue. The key assumption being that only the producer is permitted to modify the tail, and only the consumer is permitted to modify the head. Both components are permitted to read both indices. The library's atomic operations are written to ensure correctness under these assumptions, thus each function's description contains an explicit notes on its assumed caller.