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
