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
. @ .
next prev parent 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