Announce: RTEMS 5.2-rc1 Release Candidate
The RTEMS 5.2-rc1 Release Candidate is available. The release can be found at: https://ftp.rtems.org/pub/rtems/releases/5/rc/5.2-rc1/ Please follow the release instructions provided by the link. The release notes can be found here: https://ftp.rtems.org/pub/rtems/releases/5/rc/5.2-rc1/rtems-5.2-rc1-release-notes.html They detail the changes that have been made on the 5 branch. If you find a problem please raise a ticket and select the 5.2 milestone. The simplest way to create a ticket is to head to the developer Wiki at: https://devel.rtems.org/ Then click on the "Next (milestone)" link for the RTEMS 5 Release. You will need an account. Thanks Chris ___ devel mailing list devel@rtems.org http://lists.rtems.org/mailman/listinfo/devel
Re: [PATCH] aarch64/mmu: Prevent block descriptors at level -1
Tested on Versal (A72) and large mappings are now working. I have pushed the
patch.
Thanks for this. :)
Chris
On 17/11/2022 2:22 am, Kinsey Moore wrote:
> In the original implementation, level -1 was unused and all levels could
> have block-like descriptors (level 2 block descriptors are called page
> descriptors). When support for level -1 page tables was added the
> constraint on level -1 block descriptors was not honored. This prevents
> block descriptors from being mapped at level -1 since the hardware will
> not map them properly.
> ---
> bsps/aarch64/include/bsp/aarch64-mmu.h | 23 +--
> 1 file changed, 13 insertions(+), 10 deletions(-)
>
> diff --git a/bsps/aarch64/include/bsp/aarch64-mmu.h
> b/bsps/aarch64/include/bsp/aarch64-mmu.h
> index 1287c67016..ebc224b9e1 100644
> --- a/bsps/aarch64/include/bsp/aarch64-mmu.h
> +++ b/bsps/aarch64/include/bsp/aarch64-mmu.h
> @@ -243,26 +243,29 @@ BSP_START_TEXT_SECTION static inline rtems_status_code
> aarch64_mmu_map_block(
> /* check for perfect block match */
> if ( block_bottom == addr ) {
>if ( size >= chunk_size ) {
> -/* when page_flag is set the last level must be a page descriptor */
> -if ( page_flag || ( page_table[index] & MMU_DESC_TYPE_TABLE ) !=
> MMU_DESC_TYPE_TABLE ) {
> - /* no sub-table, apply block properties */
> - page_table[index] = addr | flags | page_flag;
> - size -= chunk_size;
> - addr += chunk_size;
> - continue;
> +/* level -1 can't contain block descriptors, fall through to
> subtable */
> +if ( level != -1 ) {
> + /* when page_flag is set the last level must be a page descriptor
> */
> + if ( page_flag || ( page_table[index] & MMU_DESC_TYPE_TABLE ) !=
> MMU_DESC_TYPE_TABLE ) {
> +/* no sub-table, apply block properties */
> +page_table[index] = addr | flags | page_flag;
> +size -= chunk_size;
> +addr += chunk_size;
> +continue;
> + }
> }
>} else {
> /* block starts on a boundary, but is short */
> chunk_size = size;
>
> - /* it isn't possible to go beyond page table level 2 */
> - if ( page_flag ) {
> +/* it isn't possible to go beyond page table level 2 */
> +if ( page_flag ) {
>/* no sub-table, apply block properties */
>page_table[index] = addr | flags | page_flag;
>size -= chunk_size;
>addr += chunk_size;
>continue;
> - }
> +}
>}
> } else {
>uintptr_t block_top = RTEMS_ALIGN_UP( addr, granularity );
___
devel mailing list
devel@rtems.org
http://lists.rtems.org/mailman/listinfo/devel
Question about SMP tests after shutdown
Hi, I am running testsuite applications on a dual core RISC-V CPU. When I run samples such as ticker.exe, the test ends without error messages. On SMP tests, the tests seem to run correctly and end, but there is always a fatal error from thread(s) on the other CPU. (RTEMS_FATAL_SOURCE_SMP) My guess is that the threads are being scheduled after the primary test thread shut down the RTEMS executive, causing the error to be caught. Is this expected behavior on a SMP system? There are a couple of BSPs that implement a fatal error handler to catch this error, and I would expect that on a real application, it would be handled appropriately. The error I get from smp08 is below. Thanks, Alan *** END OF TEST SMP 8 *** [ RTEMS shutdown ] CPU: 1 RTEMS version: 6.0.0.1eae6f24fec6c3ab00d8f5d0152d2a5b57ea4589 RTEMS tools: 12.2.1 20221014 (RTEMS 6, RSB e24641bda7412277c3e6490b663a12aceb093dec, Newlib 0b6342c) executing thread ID: 0x0a010002 executing thread name: TA01 *** FATAL *** fatal source: 10 (RTEMS_FATAL_SOURCE_SMP) CPU: 0 fatal code: 5 (0x0005) RTEMS version: 6.0.0.1eae6f24fec6c3ab00d8f5d0152d2a5b57ea4589 RTEMS tools: 12.2.1 20221014 (RTEMS 6, RSB e24641bda7412277c3e6490b663a12aceb093dec, Newlib 0b6342c) executing thread ID: 0x09010001 executing thread name: IDLE ___ devel mailing list devel@rtems.org http://lists.rtems.org/mailman/listinfo/devel
Re: Add Formal Verification chapter v2
Hi Andrew, I guess I was overly optimistic last night. The note on the front matter should be resolved before we push the full documentation. I guess it's a bit of chicken-and-egg but the documentation should be pushed concurrent with the software that it documents. So, when there is a `formal` folder in `rtems-central` then it makes sense to push this documentation. I think the documentation is valuable, but I'm not sure how relevant it is without the associated tooling? We probably need to rearrange this section slightly to accommodate the possibility (extant) of other formal verification approaches. I think I'd like to see Sections "9.2 Formal Tools Setup" and 9.4 through the end of the section become nested beneath "9.3 Modelling RTEMS with Promela". Add a new section 9.2 to introduce the different approaches that have/are/might be used to formally verify RTEMS. This will allow alternatives to be documented and acknowledged by the RTEMS Project. There's a bunch of terminology that is introduced in this chapter without additions to the glossary/index. I think we need some definitions added there to complement the new material. At the very least I would like to see definitions added for the keywords that are defined especially in the introduction: * semantics, formal model, artifact, refinement, LTL Once those are defined, the terms should be linked to the glossary. You can see how this is done for example in Section 5.3.4 Traceability between Software Requirements, Architecture and Design. Glossary definitions can/should link to each other as relevant. "To avoid using (long) absolute pathnames to the tools directory" ... --> maybe it makes sense for you to provide these as part of the env? Is this stuff using venv or something else? incomplete section header? "need to explain how to configure testbuilder" RTMES typo in that section In section "9.2.2 Running Test Generation" please add some notion of what is the expected output that one would be checking in the step "use a simulator to run ts-model-0.exe directly." There is overuse of double quotations throughout. Sometimes double quotes are being used to introduce terminology, avoid that. Sometimes double quotes appear in section headings, avoid that. Prefer to use double quotes only for quoting (e.g., from references or tool output). Most cases of the double quotes use in this document should be eliminated. In section "9.4 Promela to C Refinement" what is the name of the YAML file? Is there more than one, or is it unique. Some of the text that provides examples of how to do some of this might be suited to a new How-To subsection such as in the end of the "BSP Build System" section. In Section "9.6 Test Generation Maintenance" please refer to Section "Software Development Management" instead of hard-coding the patch submission process. Section 9.7 "RTEMS Formal Model Guide" seems like it includes both some aspects of a How-To but also a lot of details that might be better as a separate document specific to the Promela/Verification detailed implementation. The point of the RTEMS Software Engineering manual is to provide developers with the guidelines of how to work with RTEMS. This section is very detailed about the implementation of specific models and feels unbalanced with the rest of the new section. For example, this section is about 3/5 of the entire "Formal Verification" section. Gedare On Wed, Nov 16, 2022 at 3:57 AM andrew.butterfi...@scss.tcd.ie wrote: > > Dear Gedare, > thanks for doing this - all feedback welcome! > > Best 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: Gedare Bloom > Date: Wednesday 16 November 2022 at 02:00 > To: Chris Johns > Cc: "andrew.butterfi...@scss.tcd.ie" , > "rtems-de...@rtems.org" > Subject: Re: Add Formal Verification chapter v2 > > I plan to look at this tomorrow and will plan to push it as-is. I will > push any modifications I think should be made, or send notes back > here, after I look through it very carefully. > > On Wed, Nov 9, 2022 at 5:39 PM Chris Johns wrote: > > > > On 9/11/2022 9:48 pm, andrew.butterfi...@scss.tcd.ie wrote: > > > ping > > > > > > (my fault really, i've let this sit!) > > > > > > > Thank you for raising this and I am sorry we have not been as proactive > > as we should be. > > > > > But I have been busy, interacting with a group doing a follow-up IV&V > project with the qualification data package we produced. > > > A conseuien
Re: [PATCH] c-user: CAN framework docs
On Tue, Nov 15, 2022 at 11:14 PM Prashanth S wrote: > > Hi Gedare, > > > What are the images? > There three images: > images/c_user/CAN-framework.jpg-> Overview of CAN-Framework > images/c_user/CAN-rx-data-path.jpg -> Rx Data Path flow > images/c_user/CAN-tx-data-path.jpg -> Tx Data Path flow > We don't have many images in the docs. And as I recall we had a discussion about image formats in docs awhile back. I don't remember the details, but I think it is preferred to provide images generated from a text-based format where possible. From rtems-docs.git/README.txt, we have Images can be created from source using PlantUML and Ditaa. Please have a look to see if you can do that instead. > > This is not exactly correct. It is actually recessive where | CANH - > > CANL | < t1 for some threshold t1, > > and dominant where | CANH - CANL | > t2. And there is a gap where the > > bus is not defined at t1 < | CANH - CANL| < t2 > > This detail is not so important here, but if we're going to describe > > it then we need it to be correct. > > > > > +A 0 data bit encodes a dominant state, while a 1 data bit encodes a > > > recessive > > > +state, supporting a wired-AND convention, which gives nodes with lower ID > > > +numbers priority on the bus. > > > > I see this text has been copied from Wikipedia. This is not acceptable > > without proper attribution/reference. Please rewrite, remove, or > > reference cited material properly. Please identify if any of the below > > text is also copied from anywhere else. > > I will rewrite this text. > > > > > > + > > > +This document covers, the CAN framework and its usage by BSP CAN drivers > > > and > > Remove the comma after covers > > > typo: Initialize > > typo: Further > > I will update these typo errors. > > Regards > Prashanth S > > On Tue, 15 Nov 2022 at 20:34, Gedare Bloom wrote: >> >> Hi Prashant, >> >> What are the images? >> >> On Tue, Nov 15, 2022 at 7:49 AM Prashanth S >> wrote: >> > >> > --- >> > bsp-howto/can.rst | 201 + >> > bsp-howto/index.rst| 1 + >> > images/c_user/CAN-framework.jpg| Bin 0 -> 146625 bytes >> > images/c_user/CAN-rx-data-path.jpg | Bin 0 -> 187438 bytes >> > images/c_user/CAN-tx-data-path.jpg | Bin 0 -> 128765 bytes >> > 5 files changed, 202 insertions(+) >> > create mode 100644 bsp-howto/can.rst >> > create mode 100644 images/c_user/CAN-framework.jpg >> > create mode 100644 images/c_user/CAN-rx-data-path.jpg >> > create mode 100644 images/c_user/CAN-tx-data-path.jpg >> > >> > diff --git a/bsp-howto/can.rst b/bsp-howto/can.rst >> > new file mode 100644 >> > index 000..36d6a04 >> > --- /dev/null >> > +++ b/bsp-howto/can.rst >> > @@ -0,0 +1,201 @@ >> > +.. SPDX-License-Identifier: CC-BY-SA-4.0 >> > + >> > +.. Copyright (C) 2022 Prashanth S >> > + >> > +CAN Library >> > +*** >> > + >> > +Introduction >> > + >> > + >> > +The Controller Area Network is a robust multi-master serial communication >> > +protocol extensively used in automobiles for reliable data transfer. Two >> > or more >> > +nodes are required on the CAN network to communicate. All nodes are >> > connected to >> > +each other through a physically conventional two-wire bus. The wires are a >> > +twisted pair with a 120 Ω (nominal) characteristic impedance. >> > + >> > +This bus uses differential wired-AND signals. Two signals, CAN high >> > (CANH) and >> > +CAN low (CANL) are either driven to a "dominant" state with CANH > CANL >> > or not >> > +driven and pulled by passive resistors to a "recessive" state with CANH ≤ >> > CANL. >> This is not exactly correct. It is actually recessive where | CANH - >> CANL | < t1 for some threshold t1, >> and dominant where | CANH - CANL | > t2. And there is a gap where the >> bus is not defined at t1 < | CANH - CANL| < t2 >> This detail is not so important here, but if we're going to describe >> it then we need it to be correct. >> >> > +A 0 data bit encodes a dominant state, while a 1 data bit encodes a >> > recessive >> > +state, supporting a wired-AND convention, which gives nodes with lower ID >> > +numbers priority on the bus. >> >> I see this text has been copied from Wikipedia. This is not acceptable >> without proper attribution/reference. Please rewrite, remove, or >> reference cited material properly. Please identify if any of the below >> text is also copied from anywhere else. >> >> > + >> > +This document covers, the CAN framework and its usage by BSP CAN drivers >> > and >> Remove the comma after covers >> >> > +applications. >> > + >> > +The CAN framework allows the applications to be written in a portable >> > manner, >> > +which implies that an application can access the CAN bus without knowing >> > the >> > +details of the CAN hardware, the platform specific translations are taken >> > care >> > +by the CAN framework (So the application can focus more on the CAN >> > protocol >> > +specific implementation). >
[PATCH] aarch64/mmu: Prevent block descriptors at level -1
In the original implementation, level -1 was unused and all levels could
have block-like descriptors (level 2 block descriptors are called page
descriptors). When support for level -1 page tables was added the
constraint on level -1 block descriptors was not honored. This prevents
block descriptors from being mapped at level -1 since the hardware will
not map them properly.
---
bsps/aarch64/include/bsp/aarch64-mmu.h | 23 +--
1 file changed, 13 insertions(+), 10 deletions(-)
diff --git a/bsps/aarch64/include/bsp/aarch64-mmu.h
b/bsps/aarch64/include/bsp/aarch64-mmu.h
index 1287c67016..ebc224b9e1 100644
--- a/bsps/aarch64/include/bsp/aarch64-mmu.h
+++ b/bsps/aarch64/include/bsp/aarch64-mmu.h
@@ -243,26 +243,29 @@ BSP_START_TEXT_SECTION static inline rtems_status_code
aarch64_mmu_map_block(
/* check for perfect block match */
if ( block_bottom == addr ) {
if ( size >= chunk_size ) {
-/* when page_flag is set the last level must be a page descriptor */
-if ( page_flag || ( page_table[index] & MMU_DESC_TYPE_TABLE ) !=
MMU_DESC_TYPE_TABLE ) {
- /* no sub-table, apply block properties */
- page_table[index] = addr | flags | page_flag;
- size -= chunk_size;
- addr += chunk_size;
- continue;
+/* level -1 can't contain block descriptors, fall through to subtable
*/
+if ( level != -1 ) {
+ /* when page_flag is set the last level must be a page descriptor */
+ if ( page_flag || ( page_table[index] & MMU_DESC_TYPE_TABLE ) !=
MMU_DESC_TYPE_TABLE ) {
+/* no sub-table, apply block properties */
+page_table[index] = addr | flags | page_flag;
+size -= chunk_size;
+addr += chunk_size;
+continue;
+ }
}
} else {
/* block starts on a boundary, but is short */
chunk_size = size;
- /* it isn't possible to go beyond page table level 2 */
- if ( page_flag ) {
+/* it isn't possible to go beyond page table level 2 */
+if ( page_flag ) {
/* no sub-table, apply block properties */
page_table[index] = addr | flags | page_flag;
size -= chunk_size;
addr += chunk_size;
continue;
- }
+}
}
} else {
uintptr_t block_top = RTEMS_ALIGN_UP( addr, granularity );
--
2.30.2
___
devel mailing list
devel@rtems.org
http://lists.rtems.org/mailman/listinfo/devel
Re: Add Formal Verification chapter v2
Dear Gedare, thanks for doing this - all feedback welcome! Best 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: Gedare Bloom Date: Wednesday 16 November 2022 at 02:00 To: Chris Johns Cc: "andrew.butterfi...@scss.tcd.ie" , "rtems-de...@rtems.org" Subject: Re: Add Formal Verification chapter v2 I plan to look at this tomorrow and will plan to push it as-is. I will push any modifications I think should be made, or send notes back here, after I look through it very carefully. On Wed, Nov 9, 2022 at 5:39 PM Chris Johns wrote: > > On 9/11/2022 9:48 pm, andrew.butterfi...@scss.tcd.ie wrote: > > ping > > > > (my fault really, i've let this sit!) > > > > Thank you for raising this and I am sorry we have not been as proactive > as we should be. > > > But I have been busy, interacting with a group doing a follow-up IV&V project with the qualification data package we produced. > > A conseuience of this is that I am helping them to add two extra manager models developed by students, for Barriers and Message Queues. > > > > This would add two more entries to the model guide, and raises the question of the best place to document the models. > > Is the RTEMS Software Engineering manual the best location for those? If not, where should they live? > > > > Another side effect fo all this is that there is now a definitive version of the formal models and test generation in a public repo: > > > > https://github.com/andrewbutterfield/RTEMS-SMP-Formal > > > > Excellent. > > I have no expertise in this area and I am more than happy to defer to > you and your team in this area. > > I have no objections to this working being merge as is. I see it as > green field work and yours is the first here. I am sure updates or > changes can be made over time by you or others as the work is absorbed > and reviewed. > > Thank you for all the efforts you and those with you have made. I > personally think it is fantastic to have this work happen and being made > public in this way so thank you from me. > > Chris > ___ > devel mailing list > devel@rtems.org > http://lists.rtems.org/mailman/listinfo/devel ___ devel mailing list devel@rtems.org http://lists.rtems.org/mailman/listinfo/devel
