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!mx02.eternal-september.org!feeder.eternal-september.org!aioe.org!.POSTED!not-for-mail From: "Dmitry A. Kazakov" Newsgroups: comp.lang.ada Subject: Re: Launching background job from Ada.Real_Time.Timing_Events Date: Fri, 3 Jun 2016 14:15:57 +0200 Organization: Aioe.org NNTP Server Message-ID: References: NNTP-Posting-Host: vFKDMXWEWKqnQQwESBoFfw.user.gioia.aioe.org Mime-Version: 1.0 Content-Type: text/plain; charset=utf-8; format=flowed Content-Transfer-Encoding: 7bit X-Complaints-To: abuse@aioe.org User-Agent: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:45.0) Gecko/20100101 Thunderbird/45.1.1 X-Notice: Filtered by postfilter v. 0.8.2 Xref: news.eternal-september.org comp.lang.ada:30576 Date: 2016-06-03T14:15:57+02:00 List-Id: 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