Re: FIFO

[Niklas Holsti <niklas.holsti@tidorum.invalid>]

On 17-09-19 13:04 , Frank Buss wrote:
> On 09/19/2017 08:33 AM, Niklas Holsti wrote:
>> If one task or interrupt handler is pushing data into the buffer at some
>> rate, with some burstiness, and another task or interrupt handler is
>> pulling data from the buffer at some rate, with some burstiness, I do
>> not believe that GNATprove can show that the buffer never overflows.
>>
>> I'll be glad to be proven wrong, though.
>
> Right, this is what I meant. A real world example: This package reads
> data into my buffer:
>
> https://github.com/FrankBuss/Ada_Synth/blob/master/ada/discovery/serial_io.adb#L67
>
>
> Another unrelated problem: I think there could be a race condition, if
> the FIFO is not empty, but then the interrupt is called and the FIFO
> gets empty, and then the next byte is added to the FIFO in the else
> branch, which then will never be sent, and even worse, no more bytes at
> all will be sent after this bug. How could I prevent this? I guess I
> should disable interrupts while in the Write procedure, or is this done
> by Ada automatically because I'm in a protected body?

Yes, automatically. RM C.3.1(13): "When a handler is attached to an 
interrupt, the interrupt is blocked (subject to the Implementation 
Permission in C.3 [that is, if "the underlying system or hardware" 
allows blocking interrupts]) during the execution of every protected 
action on the protected object containing the handler."

I haven't reviewed your code in detail, but I glanced at it and wonder 
about some things:

- Serial_Port_Controller.Write checks if the Output FIFO Is_Empty, but 
it does not check if a transmission is going on. How do you intend to 
prevent the writer task(s) from calling Write too often, overwriting an 
on-going transmission with a new transmission?

- In fact, the code only puts something into the Output FIFO if the 
Output FIFO is non-empty. I assume the FIFO is empty initially, so it 
seems to me that it will always be empty. That can't be intended.

- If I understand the code correctly, 
Serial_Port_Controller.Interrupt_Handler clears the "transmission 
completed" status _after_ it has started a new transmission. This 
creates a race condition: if the UART is very fast, it might complete 
the transmission before the code clears the "transmission completed" 
status, in which case the "transmission completed" status would be lost. 
I suggest to clear the "tranmission completed" status _before_ starting 
the new transmission.

I think the protected object should have a flag variable showing if a 
transmission is going on. The flag should be set when a transmission is 
started, and be cleared in the Interrupt_Handler when it detects the 
completion of the transmission. The Write procedure should start a 
transmission if, and only if, no transmission is already going on. If a 
transmission is going on when Write is called, Write should put the Data 
into the Output FIFO, for Interrupt_Handler to transmit later.

Perhaps you intended that "not Output.Is_Empty" would mean "transmission 
going on", but that is not the way the code works. The octet currently 
being transmitted is _not_ in the Output FIFO.

(By the way, if the Rinbguffer objects are protected variables, it is 
not necessary to have pragma Volatile etc. on them, because the 
protected object does whatever is needed for multi-task access. Pragma 
Volatile etc. is needed only for _unprotected_ variables that are 
nevertheless accessed from multiple tasks.)

-- 
Niklas Holsti
Tidorum Ltd
niklas holsti tidorum fi
       .      @       .