Re: Add Formal Verification chapter v4

2023-09-22 Thread andrew.butterfi...@scss.tcd.ie 



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/ 

 




From: "andrew.butterfi...@scss.tcd.ie " 
mailto:andrew.butterfi...@scss.tcd.ie>>
Date: Thursday 21 September 2023 at 17:02

>On 21/09/2023, 16:42, "Sebastian Huber"  
>>>> wrote:
>On 21.09.23 17:41, Gedare Bloom wrote:
>>> On Thu, Sep 21, 2023 at 9:36 AM Sebastian Huber
>>> >>  
>>> >> >> wrote:
 On 21.09.23 17:28, Gedare Bloom wrote:
> I've taken a look and resolved / commented. We can leave some of the
> `sis` specific bits, with the understanding that hopefully the
> simulation target can be made more generic in the future. This could be
> a potential GSoC project for Prequalification to hook it up to
> `rtems-tools.git/tester` to make use of the capabilities we already have
> for running simulators.
 The model based tests are not target-specific. You could run them with
 any (simulator) BSP.

>>> Yes, I suspected that. However, the documentation is currently written
>>> toward sis. It may be better to point the reader to another doc that
>>> explains how to run tests, such as
>>> https://docs.rtems.org/branches/master/user/tools/tester.html 
>>>  
>>>  
>>> ;>
>>> 
>>> I don't recall any documentation that discusses simulator targets 
>>> specifically.
>>Yes, we should not duplicate this documentation. This is not maintainable.
>
>I can remove all references to `sis` from the documentation and point to 
>tester.html
>However note that the python sources for all of this, in 
>rtems-central/formal/promela/src
>we have explicit references in testbuilder-template.yml to `simulator: 
>/sparc-rtems6-sis` 
>I guess that needs to be changed.

I've referred to the RTEMS Tester, (replacing `sis`),
and also just noted that the default template for testbuilder refers to `sis`

Also, I'm not sure the best way to refer to a sub-section of another document
I used something like (See Host Tools in the RTEMS User Manual)
I guessed the URL might be less robust

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/ 
 
 
;> 

-- 
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] arm: Use a valid signed integer constant

2023-09-22 Thread Sebastian Huber 
Enumerators are restricted to signed integers in some C standards.
---
 cpukit/score/cpu/arm/include/rtems/score/cpu.h | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/cpukit/score/cpu/arm/include/rtems/score/cpu.h 
b/cpukit/score/cpu/arm/include/rtems/score/cpu.h
index 3cd43970b1..a462b48cf1 100644
--- a/cpukit/score/cpu/arm/include/rtems/score/cpu.h
+++ b/cpukit/score/cpu/arm/include/rtems/score/cpu.h
@@ -585,7 +585,7 @@ typedef enum {
   ARM_EXCEPTION_IRQ = 6,
   ARM_EXCEPTION_FIQ = 7,
   MAX_EXCEPTIONS = 8,
-  ARM_EXCEPTION_MAKE_ENUM_32_BIT = 0x
+  ARM_EXCEPTION_MAKE_ENUM_32_BIT = 0x7fff
 } Arm_symbolic_exception_name;
 
 #endif /* defined(ARM_MULTILIB_ARCH_V4) */
-- 
2.35.3

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

[PATCH] psx13: Fix use of uninitialized variable warning

2023-09-22 Thread Sebastian Huber 
---
 testsuites/psxtests/psx13/test.c | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/testsuites/psxtests/psx13/test.c b/testsuites/psxtests/psx13/test.c
index 0754dbcf30..951953ae98 100644
--- a/testsuites/psxtests/psx13/test.c
+++ b/testsuites/psxtests/psx13/test.c
@@ -639,6 +639,8 @@ static void FutimensTest( void )
   /* EBADF test case */
 
   /* Case: Pass an invalid file descriptor */
+  _Timespec_Set_to_zero( &time[0] );
+  _Timespec_Set_to_zero( &time[1] );
   rv = futimens( -1, time );
   rtems_test_assert( rv == -1 );
   rtems_test_assert( errno == EBADF );
-- 
2.35.3

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

[PATCH] tests: Add header for RTEMS test printer

2023-09-22 Thread Sebastian Huber 
The  header file is required for every RTEMS test
program.  Move the RTEMS test printer support to a dedicated header file
.  This removes an unnecessary dependency to the
RTEMS printer support in .

Tests using the RTEMS Testing Framework no longer depend on the
.
---
 cpukit/include/rtems/test-info.h  | 18 +
 cpukit/include/rtems/test-printer.h   | 69 +++
 cpukit/libtest/testbeginend.c |  1 +
 cpukit/libtest/testwrappers.c |  2 +-
 spec/build/cpukit/librtemstest.yml|  1 +
 testsuites/benchmarks/linpack/linpack-pc.c|  2 +-
 testsuites/benchmarks/whetstone/whetstone.c   |  2 +-
 testsuites/fstests/tftpfs/init.c  |  1 +
 testsuites/libtests/dl01/dl01-o1.c|  2 +-
 testsuites/libtests/dl02/dl02-o1.c|  2 +-
 testsuites/libtests/dl02/dl02-o2.c|  2 +-
 testsuites/libtests/dl05/dl05-o5.cc   |  2 +-
 testsuites/libtests/dl06/dl06-o1.c|  2 +-
 testsuites/libtests/dl06/dl06-o2.c|  2 +-
 testsuites/libtests/dl07/dl07-o1.c|  2 +-
 testsuites/libtests/dl07/dl07-o2.c|  2 +-
 testsuites/libtests/dl07/dl07-o3.c|  2 +-
 testsuites/libtests/dl07/dl07-o4.c|  2 +-
 testsuites/libtests/dl07/dl07-o5.c|  2 +-
 testsuites/libtests/dl08/dl08-o1.c|  2 +-
 testsuites/libtests/dl08/dl08-o2.c|  2 +-
 testsuites/libtests/dl08/dl08-o3.c|  2 +-
 testsuites/libtests/dl08/dl08-o4.c|  2 +-
 testsuites/libtests/dl08/dl08-o5.c|  2 +-
 .../dl08/dl08-o6-123456789-123456789.c|  2 +-
 testsuites/libtests/dl09/dl09-o1.c|  2 +-
 testsuites/libtests/dl09/dl09-o2.c|  2 +-
 testsuites/libtests/dl09/dl09-o3.c|  2 +-
 testsuites/libtests/dl09/dl09-o4.c|  2 +-
 testsuites/libtests/dl09/dl09-o5.c|  2 +-
 testsuites/libtests/dl10/dl10-o1.c|  2 +-
 testsuites/libtests/dl10/dl10-o2.c|  2 +-
 testsuites/libtests/dl10/dl10-o3.c|  2 +-
 testsuites/libtests/dl10/dl10-o4.c|  2 +-
 testsuites/libtests/dl10/dl10-o5.c|  2 +-
 testsuites/libtests/dl10/dl10-o6.c|  1 -
 testsuites/libtests/dl11/dl11-o1.c|  1 -
 testsuites/support/include/tmacros.h  |  1 +
 38 files changed, 105 insertions(+), 48 deletions(-)
 create mode 100644 cpukit/include/rtems/test-printer.h

diff --git a/cpukit/include/rtems/test-info.h b/cpukit/include/rtems/test-info.h
index c1b41ccc6e..a5c00c423a 100644
--- a/cpukit/include/rtems/test-info.h
+++ b/cpukit/include/rtems/test-info.h
@@ -3,10 +3,9 @@
 /**
  * @file
  *
- * @ingroup RTEMSTestFramework
+ * @ingroup RTEMSTest
  *
- * @brief This header file provides interfaces of the
- *   RTEMS Test Framework.
+ * @brief This header file provides interfaces of the RTEMS Test Support.
  */
 
 /*
@@ -38,7 +37,6 @@
 #define _RTEMS_TEST_H
 
 #include 
-#include 
 #include 
 #include 
 
@@ -61,11 +59,6 @@ extern "C" {
  */
 extern const char rtems_test_name[];
 
-/**
- * @brief Each test must define a printer.
- */
-extern rtems_printer rtems_test_printer;
-
 /**
  * @brief Fatal extension for tests.
  */
@@ -134,13 +127,6 @@ int rtems_test_end(const char* name);
  */
 RTEMS_NO_RETURN void rtems_test_exit(int status);
 
-/**
- * @brief Prints via the RTEMS printer.
- *
- * @return As specified by printf().
- */
-int rtems_test_printf(const char* format, ...) RTEMS_PRINTFLIKE(1, 2);
-
 #define RTEMS_TEST_PARALLEL_PROCESSOR_MAX 32
 
 typedef struct rtems_test_parallel_job rtems_test_parallel_job;
diff --git a/cpukit/include/rtems/test-printer.h 
b/cpukit/include/rtems/test-printer.h
new file mode 100644
index 00..901c7c3654
--- /dev/null
+++ b/cpukit/include/rtems/test-printer.h
@@ -0,0 +1,69 @@
+/* SPDX-License-Identifier: BSD-2-Clause */
+
+/**
+ * @file
+ *
+ * @ingroup RTEMSTest
+ *
+ * @brief This header file provides interfaces of the RTEMS Test Support.
+ */
+
+/*
+ * Copyright (C) 2014, 2023 embedded brains GmbH & Co. KG
+ *
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions
+ * are met:
+ * 1. Redistributions of source code must retain the above copyright
+ *notice, this list of conditions and the following disclaimer.
+ * 2. Redistributions in binary form must reproduce the above copyright
+ *notice, this list of conditions and the following disclaimer in the
+ *documentation and/or other materials provided with the distribution.
+ *
+ * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
+ * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
+ * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
+ * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
+ * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,

Re: [PATCH] validation: Check stack of interrupted context

2023-09-22 Thread Sebastian Huber 

On 21.09.23 16:59, Kinsey Moore wrote:

Ok, thanks! I'll take a look and see what I can find.


Thanks, I did run the test case also on riscv and it worked fine in 
uniprocessor and SMP configurations.


--
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] validation: Check stack of interrupted context

2023-09-22 Thread Kinsey Moore 
On Fri, Sep 22, 2023 at 7:44 AM Sebastian Huber <
sebastian.hu...@embedded-brains.de> wrote:

> On 21.09.23 16:59, Kinsey Moore wrote:
> > Ok, thanks! I'll take a look and see what I can find.
>
> Thanks, I did run the test case also on riscv and it worked fine in
> uniprocessor and SMP configurations.
>

Without the patch on SMP, I'm seeing a hang on "B:RtemsIntrReqRaise" on
QEMU (latest from RSB). With the patch on SMP, I'm seeing a somewhat
different assert from inside _Thread_Handler on line 139.

It seems related, so I'll keep looking into it.

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

Re: [PATCH] validation: Check stack of interrupted context

2023-09-22 Thread Kinsey Moore 
On Fri, Sep 22, 2023 at 10:46 AM Kinsey Moore 
wrote:

> On Fri, Sep 22, 2023 at 7:44 AM Sebastian Huber <
> sebastian.hu...@embedded-brains.de> wrote:
>
>> On 21.09.23 16:59, Kinsey Moore wrote:
>> > Ok, thanks! I'll take a look and see what I can find.
>>
>> Thanks, I did run the test case also on riscv and it worked fine in
>> uniprocessor and SMP configurations.
>>
>
> Without the patch on SMP, I'm seeing a hang on "B:RtemsIntrReqRaise" on
> QEMU (latest from RSB). With the patch on SMP, I'm seeing a somewhat
> different assert from inside _Thread_Handler on line 139.
>
> It seems related, so I'll keep looking into it.
>

It looks like the "msr spsel, #" directives are swapped in the wrapper
function that gets the non-interrupt stack pointer. This has the result of
corrupting the interrupt stack with a value from the non-interrupt stack
and leaving the interrupt stack in a state to continue recorrupting the
non-interrupt stack. As you can imagine, this causes some problems.
Swapping the spsel assembly seems to resolve the issue.

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

[PATCH v2 0/1] Rework JFFS2 delayed work

2023-09-22 Thread Kinsey Moore 
Changes from v1:
* Delayed work structs are now added to the chain on mount to avoid
  delayed work chain locking contention in the common case
* Delayed work structs now have pending flag that is locked
  with an internal lock to signal the need for additional work
* This integrates the change to unprotected chain manipulation

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

[PATCH v2] cpukit/jffs2: Avoid use of off-chain semantics

2023-09-22 Thread Kinsey Moore 
This reworks the JFFS2 delayed work queue to avoid use of
on-chain/off-chain semantics since they vary in behavior under
RTEMS_DEBUG and are not guaranteed to be safe to use in SMP systems.
This adds all delayed work structs to the chain on FS init and does not
remove them until umount.
---
 .../libfs/src/jffs2/include/linux/workqueue.h |  6 +-
 cpukit/libfs/src/jffs2/src/fs-rtems.c | 86 ++-
 2 files changed, 50 insertions(+), 42 deletions(-)

diff --git a/cpukit/libfs/src/jffs2/include/linux/workqueue.h 
b/cpukit/libfs/src/jffs2/include/linux/workqueue.h
index 45a2942bfc..dceb328417 100644
--- a/cpukit/libfs/src/jffs2/include/linux/workqueue.h
+++ b/cpukit/libfs/src/jffs2/include/linux/workqueue.h
@@ -2,6 +2,7 @@
 #define __LINUX_WORKQUEUE_H__
 
 #include 
+#include 
 
 struct work_struct { rtems_chain_node node; };
 
@@ -11,7 +12,6 @@ struct work_struct { rtems_chain_node node; };
 })
 
 #define INIT_DELAYED_WORK(delayed_work, delayed_workqueue_callback) ({ \
-  _Chain_Initialize_node(&(delayed_work)->work.node); \
   (delayed_work)->callback = delayed_workqueue_callback; \
 })
 
@@ -20,7 +20,9 @@ struct work_struct { rtems_chain_node node; };
 typedef void (*work_callback_t)(struct work_struct *work);
 struct delayed_work {
struct work_struct work;
-   uint64_t execution_time;
+   struct mutex dw_mutex;
+   volatile bool pending;
+   volatile uint64_t execution_time;
work_callback_t callback;
 };
 
diff --git a/cpukit/libfs/src/jffs2/src/fs-rtems.c 
b/cpukit/libfs/src/jffs2/src/fs-rtems.c
index 1a677c9772..e47f2e7fd2 100644
--- a/cpukit/libfs/src/jffs2/src/fs-rtems.c
+++ b/cpukit/libfs/src/jffs2/src/fs-rtems.c
@@ -1241,39 +1241,41 @@ rtems_chain_control delayed_work_chain;
 /* Lock for protecting the delayed work chain */
 struct mutex delayed_work_mutex;
 
-void jffs2_queue_delayed_work(struct delayed_work *work, int delay_ms)
+/*
+ * All delayed work structs are initialized and added to the chain during FS
+ * init. Must be called with no locks held
+ */
+static void add_delayed_work_to_chain(struct delayed_work *work)
 {
+   /* Initialize delayed work */
+   mutex_init(&work->dw_mutex);
+   work->pending = false;
+   _Chain_Initialize_node(&work->work.node); \
+   work->callback = NULL;
+
mutex_lock(&delayed_work_mutex);
-   if (rtems_chain_is_node_off_chain(&work->work.node)) {
-   work->execution_time = rtems_clock_get_uptime_nanoseconds() + 
delay_ms*100;
-   rtems_chain_append(&delayed_work_chain, &work->work.node);
-   }
+   rtems_chain_append_unprotected(&delayed_work_chain, &work->work.node);
mutex_unlock(&delayed_work_mutex);
 }
 
-static void jffs2_remove_delayed_work(struct delayed_work *dwork)
+void jffs2_queue_delayed_work(struct delayed_work *work, int delay_ms)
 {
-   struct delayed_work* work;
-   rtems_chain_node*node;
-
-   mutex_lock(&delayed_work_mutex);
-   if (rtems_chain_is_node_off_chain(&dwork->work.node)) {
-   mutex_unlock(&delayed_work_mutex);
-   return;
+   mutex_lock(&work->dw_mutex);
+   if (!work->pending) {
+   work->execution_time = rtems_clock_get_uptime_nanoseconds();
+   work->execution_time += delay_ms*100;
+   work->pending = true;
}
+   mutex_unlock(&work->dw_mutex);
+}
 
-   node = rtems_chain_first(&delayed_work_chain);
-   while (!rtems_chain_is_tail(&delayed_work_chain, node)) {
-   work = (struct delayed_work*) node;
-   rtems_chain_node* next_node = rtems_chain_next(node);
-   if (work == dwork) {
-   rtems_chain_extract(node);
-   mutex_unlock(&delayed_work_mutex);
-   return;
-   }
-   node = next_node;
-   }
+/* Clean up during FS unmount */
+static void jffs2_remove_delayed_work(struct delayed_work *dwork)
+{
+   mutex_lock(&delayed_work_mutex);
+   rtems_chain_extract_unprotected(&dwork->work.node);
mutex_unlock(&delayed_work_mutex);
+   /* Don't run pending delayed work, this will happen during unmount */
 }
 
 static void process_delayed_work(void)
@@ -1282,8 +1284,6 @@ static void process_delayed_work(void)
rtems_chain_node*node;
 
mutex_lock(&delayed_work_mutex);
-   rtems_chain_control process_work_chain;
-   rtems_chain_initialize_empty(&process_work_chain);
 
if (rtems_chain_is_empty(&delayed_work_chain)) {
mutex_unlock(&delayed_work_mutex);
@@ -1293,23 +1293,23 @@ static void process_delayed_work(void)
node = rtems_chain_first(&delayed_work_chain);
while (!rtems_chain_is_tail(&delayed_work_chain, node)) {
work = (struct delayed_work*) node;
-   rtems_chain_node* next_node = rtems_chain_next(node);
-   if (rtems_clock_get_uptime_nanoseconds() >= 
work->exec