From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me X-Spam-Level: X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00 autolearn=unavailable autolearn_force=no version=3.4.4 Path: eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!news.eternal-september.org!feeder.eternal-september.org!news.unit0.net!fu-berlin.de!uni-berlin.de!individual.net!not-for-mail From: Niklas Holsti Newsgroups: comp.lang.ada Subject: Re: FIFO Date: Mon, 25 Sep 2017 23:57:14 +0300 Organization: Tidorum Ltd Message-ID: References: <87wp4y8vkn.fsf@jacob-sparre.dk> <8b99f47a-63bf-4f07-9077-6dab3cf32a7f@googlegroups.com> Mime-Version: 1.0 Content-Type: text/plain; charset=utf-8; format=flowed Content-Transfer-Encoding: 7bit X-Trace: individual.net WGpVnveipBOuoqWxkwrjBQlz6stl4revX7behgfPqZ/Xeu8h5r Cancel-Lock: sha1:2S7/cUnjxpeeYxfODpF+Nl8nRno= User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.8; rv:45.0) Gecko/20100101 Thunderbird/45.8.0 In-Reply-To: Xref: news.eternal-september.org comp.lang.ada:48220 Date: 2017-09-25T23:57:14+03:00 List-Id: 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 . @ .