Re: Launching background job from Ada.Real_Time.Timing_Events

["Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de>]

On 03/06/2016 12:03, Alejandro R. Mosteo wrote:
> On 03/06/16 09:26, Dmitry A. Kazakov wrote:
>> On 02/06/2016 23:25, Alejandro R. Mosteo wrote:
>>
>>> I'm sorry but I don't follow your explanation. To make things simpler,
>>> let's consider only the 1-to-1 case. How's this protected used without a
>>> blocking operation?
>>
>> If you have FIFO, a lock-free implementation is a buffer with one read
>> and one write index (mod buffer length). The read index never advances
>> beyond the write index. Reader updates the read index and looks at the
>> write index, and conversely the writer. Indices must have pragma Atomic,
>> and the buffer not cached. For example:
>>
>> http://www.dmitry-kazakov.de/ada/components.htm#10.1.1
>
> Thanks, I was unsure if you referred to using a lock-free data type, or
> if it could be trivially done with the standard Ada containers with some
> well-known pattern I was ignorant of.

Yes, but the larger point was that using a standard container protected 
by either a monitor task or else by a protected interlocking object is 
IMO a better design that a specialized container in a protected object.

> I'll take a look at your library, I'm very interested in lock-free
> containers.
>
> A friend working on hardware architectures recently told me that a
> widely-used lock-free library (in the c++ world) had been proven with
> SPARK-like methods to be buggy. Alas, I can't remember names/dates.

That is quite possible, however I don't know what technique they used 
for making proofs. It is much about the semantics of the language 
constructs in presence of concurrent access. I am not sure about so many 
things even in Ada. I can imagine proving an implementation wrong, but 
the reverse might be exceptionally tricky. I remember reading some 
papers about this stuff, that used formal mathematical proofs, it was 
very complicated. I believe one could use a brute-force enumeration of 
possible accesses in some simulated time for making the proof in SPARK 
environment.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de