Hi Joel, Thank you for your help and clarification, this is exactly what i needed!
In terms of submitting this to the community, the situation is exactly as mentioned by Andrew. >If that statement and any others like it were deleted, >would this issue go away? I think if it's consistent and either doesn't mention nodes at all or does so on all of the directives it would definitely be more clear! >Please point out all the places where the barrier documentation >uses language from a distributed multiprocessing and shouldn't. As far as I'm aware, I've only seen nodes mentioned in Classic API Guide, in Barrier Manager Directives section: - https://docs.rtems.org/branches/master/c-user/barrier/directives.html#rtems-barrier-create - https://docs.rtems.org/branches/master/c-user/barrier/directives.html#rtems-barrier-ident - https://docs.rtems.org/branches/master/c-user/barrier/directives.html#rtems-barrier-delete Hope that helps and all the best, Jerzy pt., 28 sty 2022 o 12:00 andrew.butterfi...@scss.tcd.ie < andrew.butterfi...@scss.tcd.ie> napisał(a): > 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
