Hi Joel,
Jerzy is doing a Dissertation on this topic, and we have every plan to feed
this back into the community. The is an academic spin-off from the ESA
sponsored activity that ran for the last two years or so.
I know that the precise way we integrate this stuff back into the community
needs to be figured out, and discussion is underway about aspects of this on
the devel mailing list.
Sebastian and I hope to come to you all with a proposal regarding the Formal
Methods part - I'll let him lead that as he has a better feel for what would
fit best with community guidelines.
Regards,
Andrew
--------------------------------------------------------------------
Andrew Butterfield Tel: +353-1-896-2517 Fax: +353-1-677-2204
Lero@TCD, Head of Software Foundations & Verification Research Group
School of Computer Science and Statistics,
Room G.39, O'Reilly Institute, Trinity College, University of Dublin
http://www.scss.tcd.ie/Andrew.Butterfield/
--------------------------------------------------------------------
-----Original Message-----
From: users <users-boun...@rtems.org> on behalf of Joel Sherrill
<j...@rtems.org>
Reply to: "j...@rtems.org" <j...@rtems.org>
Date: Thursday 27 January 2022 at 23:39
To: Jerzy J <yuralogp...@gmail.com>
Cc: "rtems-us...@rtems.org" <users@rtems.org>
Subject: Re: Barrier Manager cross-node behaviour
On Thu, Jan 27, 2022 at 5:04 PM Jerzy J <yuralogp...@gmail.com> wrote:
>
> Hi,
>
> I'm using RTEMS 6 and I'm trying to model the Barrier Manager behaviour
> using Promela.
Cool! Have you modeled anything else? Is this something which could be
submitted to the community and used openly?
Just thinking anything that grows formal verification for RTEMS hopefully
helps if there is the potential for more input. Not that I am likely the
one to
build the formal model.
> However, there's one unclear thing to me which I couldn't find an exact
> explanation of in the documentation.
>
> While the `rtems_barrier_ident` directive can only search on the local
> node, if a task already had an id of the barrier from a different node,
> would it be able to call the `rtems_barrier_wait` directive on that
> barrier, or would it get INVALID_ID return code?
> In other words, can a task from one node, call directives on a barrier
from
> another node if it had an id of the barrier?
The concept of node only applies when RTEMS is built for
distributed multiprocessing. This is completely different from
the SMP support.
For distributed multiprocessing, the system model is multiple
CPUs cards on a shared bus like VMEbus with an area
of shared memory. In a distributed multiprocessing configuration,
each node is a complete RTEMS executable with an assigned
node number in the system.
For SMP, the cores are tightly integrated, share a memory
image, etc. This is considered one "node".
There is no mixing of models.
With the distributed multiprocessing, a subset of Classic API
services allow an object instance to be created with global visibility.
If global, then the ident service can be used to look up the id
for a name. For example, a task can be global. If created on
node 1, a task on node 2 can change its priority.
I doubt you really care about the distributed multiprocessing
configuration but even if you did, barriers are local only and
can't be accessed by other nodes in a distributed
processing configuration.
> I would also assume that behaviour would be consistent for `delete` and
> `release` directives as well? Although it is mentioned in the `delete`
> directive constraints that only local tasks can delete a barrier, in other
> directives it is not listed as a constraint.
That is probably just an artifact of copying the starting point for
the documentation from another API class that did support
being global.
If that statement and any others like it were deleted,
would this issue go away?
Please point out all the places where the barrier documentation
uses language from a distributed multiprocessing and shouldn't.
Thanks.
--joel
> Thanks you in advance and all the best,
> Jerzy
> _______________________________________________
> users mailing list
> users@rtems.org
> http://lists.rtems.org/mailman/listinfo/users
_______________________________________________
users mailing list
users@rtems.org
http://lists.rtems.org/mailman/listinfo/users
_______________________________________________
users mailing list
users@rtems.org
http://lists.rtems.org/mailman/listinfo/users
