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=-0.9 required=5.0 tests=BAYES_00,FORGED_GMAIL_RCVD, FREEMAIL_FROM autolearn=no autolearn_force=no version=3.4.4 X-Google-Thread: 103376,1ce6fddc56263182 X-Google-Attributes: gid103376,public,usenet X-Google-Language: ENGLISH,ASCII-7-bit Path: g2news2.google.com!postnews.google.com!r34g2000hsd.googlegroups.com!not-for-mail From: Maciej Sobczak Newsgroups: comp.lang.ada Subject: Re: Ravenscar and run-time program parameters Date: Mon, 03 Sep 2007 02:29:51 -0700 Organization: http://groups.google.com Message-ID: <1188811791.024251.105590@r34g2000hsd.googlegroups.com> References: <1188373703.936484.105650@w3g2000hsg.googlegroups.com> <1188456764.786015.30640@o80g2000hse.googlegroups.com> NNTP-Posting-Host: 137.138.37.241 Mime-Version: 1.0 Content-Type: text/plain; charset="us-ascii" X-Trace: posting.google.com 1188811791 27355 127.0.0.1 (3 Sep 2007 09:29:51 GMT) X-Complaints-To: groups-abuse@google.com NNTP-Posting-Date: Mon, 3 Sep 2007 09:29:51 +0000 (UTC) In-Reply-To: User-Agent: G2/1.0 X-HTTP-UserAgent: Mozilla/5.0 (X11; U; Linux i686; en-US; rv:1.8.0.12) Gecko/20070724 Red Hat/1.5.0.12-0.3.slc3 Firefox/1.5.0.12,gzip(gfe),gzip(gfe) Complaints-To: groups-abuse@google.com Injection-Info: r34g2000hsd.googlegroups.com; posting-host=137.138.37.241; posting-account=ps2QrAMAAAA6_jCuRt2JEIpn5Otqf_w0 Xref: g2news2.google.com comp.lang.ada:1671 Date: 2007-09-03T02:29:51-07:00 List-Id: On 31 Sie, 11:01, Xavier Nicollin wrote: > I suppose you are talking about Example 12 (p. 32). I believe (and I hope!) > it is correct: the two calls to Suspend_Until_True take place in the > regular procedures (Place_Item and Extract_Item), and not in the protected > ones (Place and Extract). When I think about it example a bit more, I conclude that it is kind of cheating. The Ravenspark profile was created to establish the practice that helps with code analysis and verification. Protected object with two entries was considered too much to be analysable and the trick is proposed to do exactly the same, just with a bit different spelling: instead of protected object with many entries one has to use a package with many blocking procedures - and the blocking is performed on nothing else than simple boolean barriers (suspension objects are just this). I cannot stop myself from asking: what makes is easier to analyze? Actually, I find this example more *difficult* to analyze, because it uses the multi-phase approach for performing the single action (try and then see what happened and then potentially repeat). The fact that the single action is attempted twice does not make it any easier for me. Also, in the second attempt the OK out variable is assigned but never read after that. Nobody is bothered by this data flow issue? Am I missing something? What about another variant: a package with many procedures that block on private semaphore protected object before doing the requested action? It's still cheating, but at least the multi-phase operation and the data flow issue are gone. -- Maciej Sobczak http://www.msobczak.com/