comp.lang.ada
 help / color / mirror / Atom feed
From: Niklas Holsti <niklas.holsti@tidorum.invalid>
Subject: Re: Scheduling behaviour issue
Date: Thu, 23 Apr 2020 00:58:49 +0300
Date: 2020-04-23T00:58:49+03:00	[thread overview]
Message-ID: <hgbt0pFf4o0U1@mid.individual.net> (raw)
In-Reply-To: <c246151d-600a-4262-a7ee-e6233a344333@googlegroups.com>

On 2020-04-22 23:41, AdaMagica wrote:
> Am Mittwoch, 22. April 2020 20:03:56 UTC+2 schrieb Niklas Holsti:
>> Under RTEMS, if there are higher-priority tasks on that processor core,
>> such actions on shared data would not have this mutual-exclusion
>> property, and the shared data could be messed up. However, I'm not sure
>> if such use of shared data is "correct" per the Ada RM, and if the
>> resulting mess can be called "misbehaviour".
> 
> This is the reasoning of Ada 83 (RM 9.11 Shared Variables):

    [snipped]

> I'm too lazy to search for the relevant text in current Ada, but as
> far as I can tell, this principle is still valid.

The wording in Ada 2012 is very different (RM 9.10 Shared Variables, and 
C.6 Shared Variable Control).

As I understand it, two tasks can read and/or write shared atomic 
variables without that being erroneous, and all tasks see the same order 
of operations on each variable separately, but the interleaving order of 
these reads and writes from the two tasks is not specified (if the 
reads/writes are not in a protected operation or similar).

Mutual exclusion for actions on shared data is usually necessary to 
ensure that a _sequence_ of reads/writes done by one task is not 
_interleaved_ with reads/writes from another task. As far as I can see, 
RM 9.10 and C.6 (and Ada 83 RM 9.11) do not address that question.

The usual example is a simple increment of an atomic counter variable 
(read - add one - write):

    Counter := Counter + 1;

which can lose one count if executed interleaved by two tasks. However, 
if the two tasks have the same priority, and compete for the same 
processor, and the Ada rule quoted by Simon (D.2.3(9)) applies, then 
both tasks can execute the increment without risking interleaving, or so 
it seems to me. But if the RTEMS rule is followed, then pre-emptions 
from higher-priority tasks can force interleaving of instructions from 
the two incrementing tasks, and thus break the counter.

> This is one of the reasons I guess that protected objects were
> introduced.
Certainly (and why rendez-vous parameters were introduced in Ada 83) and 
I would definitely recommend using protected objects for shared 
counters. That would make the counters work properly even under RTEMS.

Simon's challenge was to find a correct program that misbehaves under 
the RTEMS scheduling rule. I think my example will misbehave (not work 
as the programmer expected) but I'm not fully sure if the Ada RM defines 
its behaviour even under the Ada rules. I'm looking for an RM rule that 
says that if two tasks have the same priority and are scheduled on the 
same processor then only one task is running at a time, and executes all 
its reads/writes without any interleaved reads/writes from the other 
task, until the running task somehow yields to the other task. This may 
be implicit in the notions of "scheduling" and "running", but I would 
prefer an explicit connection between those notions and RM 9.10 and C.6.

In this connection I want to ask if the "Discussion" in RM 2012 
9.10(15.b) uses a valid example. The Discussion says that two 
"sequential" assignments to the same variable, where neither "signals" 
the other, are not erroneous, because there may be cases where the order 
in which the assignments are executed makes no difference. The 
Discussion gives, as an example, assignments that just "accumulate 
aggregate counts". It seems to me that the order of two such assignments 
to the same counter does matter, because the values written may be 
different, as in the counter-increment example above. Am I right? If so, 
this example seems wrong for this Discussion (also in Ada 202X ARM).

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

  reply	other threads:[~2020-04-22 21:58 UTC|newest]

Thread overview: 14+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2020-04-22 11:34 Scheduling behaviour issue Simon Wright
2020-04-22 16:16 ` fabien.chouteau
2020-04-22 17:20   ` Simon Wright
2020-04-22 18:05     ` Anh Vo
2020-04-22 18:21       ` Niklas Holsti
2020-04-22 18:03 ` Niklas Holsti
2020-04-22 20:41   ` AdaMagica
2020-04-22 21:58     ` Niklas Holsti [this message]
2020-04-23  0:47       ` Jere
2020-04-23 10:56   ` Simon Wright
2020-04-23 12:38     ` Niklas Holsti
2020-04-23 12:57     ` Niklas Holsti
2020-04-23 11:48 ` Simon Wright
2020-04-23 13:18 ` Niklas Holsti
replies disabled

This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox