Barrier Manager cross-node behaviour

[Andrew.Butterfield at scss.tcd.ie]

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 at 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-bounces at rtems.org> on behalf of Joel Sherrill <joel at rtems.org>
Reply to: "joel at rtems.org" <joel at rtems.org>
Date: Thursday 27 January 2022 at 23:39
To: Jerzy J <yuralogplus at gmail.com>
Cc: "rtems-users at rtems.org" <users at rtems.org>
Subject: Re: Barrier Manager cross-node behaviour

    On Thu, Jan 27, 2022 at 5:04 PM Jerzy J <yuralogplus at 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 at rtems.org
    > http://lists.rtems.org/mailman/listinfo/users
    _______________________________________________
    users mailing list
    users at rtems.org
    http://lists.rtems.org/mailman/listinfo/users