Re: [PATCH 00/18] Adds Formal Verification Material

[Sebastian Huber]

Hello Andrew,

On 22/12/2022 12:29, andrew.butterfi...@scss.tcd.ie wrote:

 From 3390ccc51f46ce0a4baa60422a62530c7c3c29bd Mon Sep 17 00:00:00 2001
From: Andrew Butterfield
Date: Wed, 21 Dec 2022 18:03:47 +
Subject: [PATCH 00/18] Adds Formal Verification Material

This patch-set adds in the Promela/SPIN models and tools developed as part of
the ESA-sponsored activity "Qualification of RTEMS Symmetric Multiprocessing
(SMP)" as well as result of ongoing contributions by students at Trinity College
Dublin to improve and extend them.

It is a subset of the material contained at
   https://github.com/andrewbutterfield/RTEMS-SMP-Formal

It focusses in the main on what currently produces RTEMS test code.


thanks for the patch set. I was about to review it and noticed that not 
all patches did show up on the mailing list probably due to the mailing 
list size limit.


I added the rtems-central repository to the Github site:

https://github.com/RTEMS/rtems-central

Could you please fork this repository, add a branch with your patches to 
your fork, and then open a pull request?


--
embedded brains GmbH
Herr Sebastian HUBER
Dornierstr. 4
82178 Puchheim
Germany
email: sebastian.hu...@embedded-brains.de
phone: +49-89-18 94 741 - 16
fax:   +49-89-18 94 741 - 08

Registergericht: Amtsgericht München
Registernummer: HRB 157899
Vertretungsberechtigte Geschäftsführer: Peter Rasmussen, Thomas Dörfler
Unsere Datenschutzerklärung finden Sie hier:
https://embedded-brains.de/datenschutzerklaerung/
___
devel mailing list
devel@rtems.org
http://lists.rtems.org/mailman/listinfo/devel

Re: [PATCH 00/18] Adds Formal Verification Material

[andrew.butterfi...@scss.tcd.ie]

Hello Sebastian,

 Yes - I noticed that problem - I got a lot of responses about those emails 
being referred to the moderator.

Some of those blocked patches were adding in archive material. I did this 
because of recent interactions
with the follow-up ESA project looking at Independent Validation and 
Verification (IV&V). They didn't just 
want to see the starting models and final test code and results, but also all 
the intermediate artifacts.
This can be quite a large amount of data. 

On reflection, it may not make much sense to include this stuff 
- rather the proposed new section in the Software Engineering Manual should 
mention the need to make 
such archives available.

I'll do the fork/patch/PR as you suggested (I can leave the archive stuff out - 
it's generated by the tooling anyway).

Best regards, and Happy New Year,

 Andrew



On 03/01/2023, 09:11, "Sebastian Huber" mailto:sebastian.hu...@embedded-brains.de>> wrote:


Hello Andrew,


On 22/12/2022 12:29, andrew.butterfi...@scss.tcd.ie 
 wrote:
> From 3390ccc51f46ce0a4baa60422a62530c7c3c29bd Mon Sep 17 00:00:00 2001
> From: Andrew Butterfield >
> Date: Wed, 21 Dec 2022 18:03:47 +
> Subject: [PATCH 00/18] Adds Formal Verification Material
> 
> This patch-set adds in the Promela/SPIN models and tools developed as part of
> the ESA-sponsored activity "Qualification of RTEMS Symmetric Multiprocessing
> (SMP)" as well as result of ongoing contributions by students at Trinity 
> College
> Dublin to improve and extend them.
> 
> It is a subset of the material contained at
> https://github.com/andrewbutterfield/RTEMS-SMP-Formal 
> 
> 
> It focusses in the main on what currently produces RTEMS test code.


thanks for the patch set. I was about to review it and noticed that not 
all patches did show up on the mailing list probably due to the mailing 
list size limit.


I added the rtems-central repository to the Github site:


https://github.com/RTEMS/rtems-central 


Could you please fork this repository, add a branch with your patches to 
your fork, and then open a pull request?


-- 
embedded brains GmbH
Herr Sebastian HUBER
Dornierstr. 4
82178 Puchheim
Germany
email: sebastian.hu...@embedded-brains.de 

phone: +49-89-18 94 741 - 16
fax: +49-89-18 94 741 - 08


Registergericht: Amtsgericht München
Registernummer: HRB 157899
Vertretungsberechtigte Geschäftsführer: Peter Rasmussen, Thomas Dörfler
Unsere Datenschutzerklärung finden Sie hier:
https://embedded-brains.de/datenschutzerklaerung/ 




___
devel mailing list
devel@rtems.org
http://lists.rtems.org/mailman/listinfo/devel

Re: [PATCH 00/18] Adds Formal Verification Material

[Sebastian Huber]

Hello Andrew,

I wish you also a Happy New Year.

On 03/01/2023 12:42, andrew.butterfi...@scss.tcd.ie wrote:

Hello Sebastian,

  Yes - I noticed that problem - I got a lot of responses about those emails 
being referred to the moderator.

Some of those blocked patches were adding in archive material. I did this 
because of recent interactions
with the follow-up ESA project looking at Independent Validation and Verification 
(IV&V). They didn't just
want to see the starting models and final test code and results, but also all 
the intermediate artifacts.
This can be quite a large amount of data.

On reflection, it may not make much sense to include this stuff
- rather the proposed new section in the Software Engineering Manual should 
mention the need to make
such archives available.

I'll do the fork/patch/PR as you suggested (I can leave the archive stuff out - 
it's generated by the tooling anyway).


As a rule of thumb, generated stuff should not be included in the 
repository. However, the user of the repository should be able to 
regenerate everything in its own environment.


--
embedded brains GmbH
Herr Sebastian HUBER
Dornierstr. 4
82178 Puchheim
Germany
email: sebastian.hu...@embedded-brains.de
phone: +49-89-18 94 741 - 16
fax:   +49-89-18 94 741 - 08

Registergericht: Amtsgericht München
Registernummer: HRB 157899
Vertretungsberechtigte Geschäftsführer: Peter Rasmussen, Thomas Dörfler
Unsere Datenschutzerklärung finden Sie hier:
https://embedded-brains.de/datenschutzerklaerung/
___
devel mailing list
devel@rtems.org
http://lists.rtems.org/mailman/listinfo/devel

[PATCH] bsps/xil: Use the LP64 header for ILP32

[Kinsey Moore]

Xilinx's upstream ILP32 xil_cache.h header is out of date and broken.
This provides a copy of the LP64 header in place of the ILP32 header
since the LP64 header includes all the correct types to work with either
data model.
---
 bsps/include/xil/arm/ARMv8/32bit/xil_cache.h | 35 ++--
 1 file changed, 25 insertions(+), 10 deletions(-)

diff --git a/bsps/include/xil/arm/ARMv8/32bit/xil_cache.h 
b/bsps/include/xil/arm/ARMv8/32bit/xil_cache.h
index 0fe994b093..b878d05299 100644
--- a/bsps/include/xil/arm/ARMv8/32bit/xil_cache.h
+++ b/bsps/include/xil/arm/ARMv8/32bit/xil_cache.h
@@ -1,5 +1,5 @@
 /**
-* Copyright (c) 2015 - 2020 Xilinx, Inc.  All rights reserved.
+* Copyright (c) 2014 - 2021 Xilinx, Inc.  All rights reserved.
 * SPDX-License-Identifier: MIT
 **/
 
@@ -8,7 +8,7 @@
 *
 * @file xil_cache.h
 *
-* @addtogroup a53_32_cache_apis Cortex A53 32bit Processor Cache Functions
+* @addtogroup a53_64_cache_apis Cortex A53 64bit Processor Cache Functions
 *
 * Cache functions provide access to cache related operations such as flush
 * and invalidate for instruction and data caches. It gives option to perform
@@ -22,7 +22,7 @@
 *
 * Ver   Who  Date Changes
 * -   ---
-* 5.2  pkp  28/05/15 First release
+* 5.00 pkp  05/29/14 First release
 * 
 *
 **/
@@ -35,21 +35,36 @@
 extern "C" {
 #endif
 
+/**
+ *@cond nocomments
+ */
+
+/** Constant Definitions */
+#define L1_DATA_PREFETCH_CONTROL_MASK  0xE000
+#define L1_DATA_PREFETCH_CONTROL_SHIFT  13
+
+/**
+ *@endcond
+ */
+
+/* Macros (Inline Functions) Definitions */
+#define Xil_DCacheFlushRange Xil_DCacheInvalidateRange
+
+/** Function Prototypes **/
 void Xil_DCacheEnable(void);
 void Xil_DCacheDisable(void);
 void Xil_DCacheInvalidate(void);
-void Xil_DCacheInvalidateRange(INTPTR adr, u32 len);
+void Xil_DCacheInvalidateRange(INTPTR adr, INTPTR len);
+void Xil_DCacheInvalidateLine(INTPTR adr);
 void Xil_DCacheFlush(void);
-void Xil_DCacheFlushRange(INTPTR adr, u32 len);
-void Xil_DCacheInvalidateLine(u32 adr);
-void Xil_DCacheFlushLine(u32 adr);
+void Xil_DCacheFlushLine(INTPTR adr);
 
-void Xil_ICacheInvalidateLine(u32 adr);
 void Xil_ICacheEnable(void);
 void Xil_ICacheDisable(void);
 void Xil_ICacheInvalidate(void);
-void Xil_ICacheInvalidateRange(INTPTR adr, u32 len);
-
+void Xil_ICacheInvalidateRange(INTPTR adr, INTPTR len);
+void Xil_ICacheInvalidateLine(INTPTR adr);
+void Xil_ConfigureL1Prefetch(u8 num);
 #ifdef __cplusplus
 }
 #endif
-- 
2.30.2

___
devel mailing list
devel@rtems.org
http://lists.rtems.org/mailman/listinfo/devel

Ticket 4364

[zack leung]

Hello,

I'm currently looking at ticket 4364. It says that there is a difference
between the test results printed by the console and what is emailed to
@devel. I don't see a difference and i'm just wondering if it has been
fixed

Zack
___
devel mailing list
devel@rtems.org
http://lists.rtems.org/mailman/listinfo/devel