spec: Specify the system termination

8 files changed, 403 insertions, 0 deletions

diff --git a/spec/score/interr/req/terminate-halt.yml b/spec/score/interr/req/terminate-halt.yml
new file mode 100644
index 00000000..85759ba8
--- /dev/null
+++ b/spec/score/interr/req/terminate-halt.yml
@@ -0,0 +1,16 @@
+SPDX-License-Identifier: CC-BY-SA-4.0
+copyrights:
+- Copyright (C) 2021 embedded brains GmbH (http://www.embedded-brains.de)
+enabled-by:
+  not: RTEMS_SMP
+links:
+- role: requirement-refinement
+  uid: terminate
+functional-type: function
+rationale: null
+references: []
+requirement-type: functional
+text: |
+  While ${../if/terminate:/name} executes, when the system state was set, the
+  system shall halt.
+type: requirement
diff --git a/spec/score/interr/req/terminate-shutdown-halt.yml b/spec/score/interr/req/terminate-shutdown-halt.yml
new file mode 100644
index 00000000..9b014bf8
--- /dev/null
+++ b/spec/score/interr/req/terminate-shutdown-halt.yml
@@ -0,0 +1,15 @@
+SPDX-License-Identifier: CC-BY-SA-4.0
+copyrights:
+- Copyright (C) 2021 embedded brains GmbH (http://www.embedded-brains.de)
+enabled-by: RTEMS_SMP
+links:
+- role: requirement-refinement
+  uid: terminate
+functional-type: function
+rationale: null
+references: []
+requirement-type: functional
+text: |
+  While ${../if/terminate:/name} executes, when the shutdown request was
+  issued, the system shall halt.
+type: requirement
diff --git a/spec/score/interr/req/terminate-shutdown.yml b/spec/score/interr/req/terminate-shutdown.yml
new file mode 100644
index 00000000..976e73f5
--- /dev/null
+++ b/spec/score/interr/req/terminate-shutdown.yml
@@ -0,0 +1,15 @@
+SPDX-License-Identifier: CC-BY-SA-4.0
+copyrights:
+- Copyright (C) 2021 embedded brains GmbH (http://www.embedded-brains.de)
+enabled-by: RTEMS_SMP
+links:
+- role: requirement-refinement
+  uid: terminate
+functional-type: function
+rationale: null
+references: []
+requirement-type: functional
+text: |
+  While ${../if/terminate:/name} executes, when the system state was set, a
+  shutdown request to all configured processors shall be issued.
+type: requirement
diff --git a/spec/score/interr/req/terminate-state.yml b/spec/score/interr/req/terminate-state.yml
new file mode 100644
index 00000000..c4f01b99
--- /dev/null
+++ b/spec/score/interr/req/terminate-state.yml
@@ -0,0 +1,15 @@
+SPDX-License-Identifier: CC-BY-SA-4.0
+copyrights:
+- Copyright (C) 2021 embedded brains GmbH (http://www.embedded-brains.de)
+enabled-by: true
+links:
+- role: requirement-refinement
+  uid: terminate
+functional-type: function
+rationale: null
+references: []
+requirement-type: functional
+text: |
+  While ${../if/terminate:/name} executes, when the fatal extensions were
+  invoked, the system state shall be set to terminated.
+type: requirement
diff --git a/spec/score/interr/req/terminate-userext.yml b/spec/score/interr/req/terminate-userext.yml
new file mode 100644
index 00000000..ba880d1a
--- /dev/null
+++ b/spec/score/interr/req/terminate-userext.yml
@@ -0,0 +1,16 @@
+SPDX-License-Identifier: CC-BY-SA-4.0
+copyrights:
+- Copyright (C) 2021 embedded brains GmbH (http://www.embedded-brains.de)
+enabled-by: true
+links:
+- role: requirement-refinement
+  uid: terminate
+functional-type: function
+rationale: null
+references: []
+requirement-type: functional
+text: |
+  When ${../if/terminate:/name} is called, the fatal extensions shall be
+  invoked in ${/glossary/extension-forward-order:/term} with the fatal source
+  and fatal code specified by the respective parameter.
+type: requirement
diff --git a/spec/score/interr/req/terminate.yml b/spec/score/interr/req/terminate.yml
new file mode 100644
index 00000000..f93ca816
--- /dev/null
+++ b/spec/score/interr/req/terminate.yml
@@ -0,0 +1,16 @@
+SPDX-License-Identifier: CC-BY-SA-4.0
+copyrights:
+- Copyright (C) 2021 embedded brains GmbH (http://www.embedded-brains.de)
+enabled-by: true
+links:
+- role: requirement-refinement
+  uid: /req/fatal-error
+- role: interface-function
+  uid: ../if/terminate
+functional-type: function
+rationale: null
+references: []
+requirement-type: functional
+text: |
+  The ${../if/terminate:/name} function shall terminate the system.
+type: requirement
diff --git a/spec/score/interr/val/terminate.yml b/spec/score/interr/val/terminate.yml
new file mode 100644
index 00000000..273ab3c7
--- /dev/null
+++ b/spec/score/interr/val/terminate.yml
@@ -0,0 +1,279 @@
+SPDX-License-Identifier: CC-BY-SA-4.0 OR BSD-2-Clause
+copyrights:
+- Copyright (C) 2021 embedded brains GmbH (http://www.embedded-brains.de)
+enabled-by: true
+links: []
+test-actions:
+- action-brief: |
+    Create two dynamic extensions.  Call the system termination procedure.
+    Delete the two dynamic extensions.
+  action-code: |
+    rtems_status_code      sc;
+    rtems_extensions_table table;
+    rtems_id               id_2;
+    rtems_id               id_3;
+    bool                   shutdown_ok;
+
+    #if defined(RTEMS_SMP)
+    shutdown_ok = ( _Per_CPU_Get_state( _Per_CPU_Get() ) == PER_CPU_STATE_UP );
+    #else
+    shutdown_ok = true;
+    #endif
+
+    memset( &table, 0, sizeof( table ) );
+
+    table.fatal = FatalExtension2;
+    sc = rtems_extension_create(
+      rtems_build_name( ' ', ' ', ' ', '2' ),
+      &table,
+      &id_2
+    );
+    T_step_rsc_success( ${step}, sc );
+
+    table.fatal = FatalExtension3;
+    sc = rtems_extension_create(
+      rtems_build_name( ' ', ' ', ' ', '3' ),
+      &table,
+      &id_3
+    );
+    T_step_rsc_success( ${step}, sc );
+
+    test_case_active = true;
+
+    if ( setjmp( before_terminate ) == 0 ) {
+      _Terminate( RTEMS_FATAL_SOURCE_APPLICATION, 123456 );
+    }
+
+    test_case_active = false;
+
+    sc = rtems_extension_delete( id_2 );
+    T_step_rsc_success( ${step}, sc );
+
+    sc = rtems_extension_delete( id_3 );
+    T_step_rsc_success( ${step}, sc );
+  checks:
+  - brief: |
+      Check that the fatal user extensions were called with the expected
+      source.
+    code: |
+      T_step_eq_int(
+        ${step},
+        info[ 0 ].source,
+        RTEMS_FATAL_SOURCE_APPLICATION
+      );
+      T_step_eq_int(
+        ${step},
+        info[ 1 ].source,
+        RTEMS_FATAL_SOURCE_APPLICATION
+      );
+      T_step_eq_int(
+        ${step},
+        info[ 2 ].source,
+        RTEMS_FATAL_SOURCE_APPLICATION
+      );
+      T_step_eq_int(
+        ${step},
+        info[ 3 ].source,
+        RTEMS_FATAL_SOURCE_APPLICATION
+      );
+    links:
+    - role: validation
+      uid: terminate-userext
+  - brief: |
+      Check that the fatal user extensions were called with the expected always
+      set to false argument.
+    code: |
+      T_step_false( ${step}, info[ 0 ].always_set_to_false );
+      T_step_false( ${step}, info[ 1 ].always_set_to_false );
+      T_step_false( ${step}, info[ 2 ].always_set_to_false );
+      T_step_false( ${step}, info[ 3 ].always_set_to_false );
+    links:
+    - role: validation
+      uid: terminate-userext
+  - brief: |
+      Check that the fatal user extensions were called with the expected code.
+    code: |
+      T_step_eq_ulong( ${step}, info[ 0 ].code, 123456 );
+      T_step_eq_ulong( ${step}, info[ 1 ].code, 123456 );
+      T_step_eq_ulong( ${step}, info[ 2 ].code, 123456 );
+      T_step_eq_ulong( ${step}, info[ 3 ].code, 123456 );
+    links:
+    - role: validation
+      uid: terminate-userext
+  - brief: |
+      Check that the fatal user extensions were called in forward order.
+    code: |
+      T_step_eq_uint( ${step}, info[ 0 ].counter, 1 );
+      T_step_eq_uint( ${step}, info[ 1 ].counter, 2 );
+      T_step_eq_uint( ${step}, info[ 2 ].counter, 3 );
+      T_step_eq_uint( ${step}, info[ 3 ].counter, 4 );
+    links:
+    - role: validation
+      uid: terminate-userext
+  - brief: |
+      Check that the system state is terminated.
+    code: |
+      T_step_eq_int( ${step}, _System_state_Get(), SYSTEM_STATE_TERMINATED );
+    links:
+    - role: validation
+      uid: terminate-state
+  - brief: |
+      Where the system was built with SMP support enabled, check that a
+      shutdown request was issued.
+    code: |
+      #if defined(RTEMS_SMP)
+      shutdown_ok = ( shutdown_ok && _ISR_Get_level() != 0 &&
+        _Per_CPU_Get_state( _Per_CPU_Get() ) == PER_CPU_STATE_SHUTDOWN );
+      _ISR_Set_level( 0 );
+      #endif
+      T_step_true( ${step}, shutdown_ok );
+    links:
+    - role: validation
+      uid: terminate-shutdown
+  - brief: |
+      Check that the system was halted with the expected fatal source.
+    code: |
+      T_step_eq_int( ${step}, halt_source, RTEMS_FATAL_SOURCE_APPLICATION );
+    links:
+    - role: validation
+      uid: terminate-halt
+    - role: validation
+      uid: terminate-shutdown-halt
+  - brief: |
+      Check that the system was halted with the expected fatal code.
+    code: |
+      T_step_eq_ulong( ${step}, halt_code, 123456 );
+    links:
+    - role: validation
+      uid: terminate-halt
+    - role: validation
+      uid: terminate-shutdown-halt
+  - brief: |
+      Check that the system was finally halted.
+    code: |
+      T_step_eq_uint( ${step}, counter, 5 );
+    links:
+    - role: validation
+      uid: terminate-halt
+    - role: validation
+      uid: terminate-shutdown-halt
+  links:
+  - role: validation
+    uid: ../req/terminate
+test-brief: |
+  Tests system termination procedure.
+test-context: []
+test-context-support: null
+test-description: null
+test-header: null
+test-includes:
+- bsp.h
+- rtems/score/atomic.h
+- rtems/score/percpu.h
+- rtems/score/sysstate.h
+- setjmp.h
+- string.h
+test-local-includes:
+- tc-terminate.h
+test-setup: null
+test-stop: null
+test-support: |
+  typedef struct {
+    unsigned int       counter;
+    rtems_fatal_source source;
+    bool               always_set_to_false;
+    rtems_fatal_code   code;
+  } FatalInfo;
+
+  static Atomic_Uint counter;
+
+  static FatalInfo info[ 4 ];
+
+  static bool test_case_active;
+
+  static const rtems_extensions_table bsp = BSP_INITIAL_EXTENSION;
+
+  static jmp_buf before_terminate;
+
+  static unsigned int halt_counter;
+
+  static rtems_fatal_source halt_source;
+
+  static rtems_fatal_code halt_code;
+
+  static unsigned int GetCounter( void )
+  {
+    return _Atomic_Fetch_add_uint( &counter, 1, ATOMIC_ORDER_RELAXED ) + 1;
+  }
+
+  void __real__CPU_Fatal_halt( uint32_t source, CPU_Uint32ptr code );
+
+  void __wrap__CPU_Fatal_halt( uint32_t source, CPU_Uint32ptr code );
+
+  void __wrap__CPU_Fatal_halt( uint32_t source, CPU_Uint32ptr code )
+  {
+    if ( test_case_active ) {
+      halt_counter = GetCounter();
+      halt_source = source;
+      halt_code = code;
+      longjmp( before_terminate, 1 );
+    } else {
+      __real__CPU_Fatal_halt( source, code );
+    }
+  }
+
+  static void FatalExtension(
+    rtems_fatal_source source,
+    bool               always_set_to_false,
+    rtems_fatal_code   code,
+    size_t             index
+  )
+  {
+    if ( test_case_active ) {
+      info[ index ].counter = GetCounter();
+      info[ index ].source = source;
+      info[ index ].always_set_to_false = always_set_to_false;
+      info[ index ].code = code;
+    } else {
+      ( *bsp.fatal )( source, always_set_to_false, code );
+    }
+  }
+
+  void FatalExtension0(
+    rtems_fatal_source source,
+    bool               always_set_to_false,
+    rtems_fatal_code   code
+  )
+  {
+    FatalExtension( source, always_set_to_false, code, 0 );
+  }
+
+  void FatalExtension1(
+    rtems_fatal_source source,
+    bool               always_set_to_false,
+    rtems_fatal_code   code
+  )
+  {
+    FatalExtension( source, always_set_to_false, code, 1 );
+  }
+
+  static void FatalExtension2(
+    rtems_fatal_source source,
+    bool               always_set_to_false,
+    rtems_fatal_code   code
+  )
+  {
+    FatalExtension( source, always_set_to_false, code, 2 );
+  }
+
+  static void FatalExtension3(
+    rtems_fatal_source source,
+    bool               always_set_to_false,
+    rtems_fatal_code   code
+  )
+  {
+    FatalExtension( source, always_set_to_false, code, 3 );
+  }
+test-target: testsuites/validation/tc-terminate.c
+test-teardown: null
+type: test-case
diff --git a/spec/testsuites/terminate.yml b/spec/testsuites/terminate.yml
new file mode 100644
index 00000000..555947c4
--- /dev/null
+++ b/spec/testsuites/terminate.yml
@@ -0,0 +1,31 @@
+SPDX-License-Identifier: CC-BY-SA-4.0 OR BSD-2-Clause
+copyrights:
+- Copyright (C) 2021 embedded brains GmbH (http://www.embedded-brains.de)
+enabled-by: true
+links:
+- role: requirement-refinement
+  uid: /req/test-suites
+- role: validation
+  uid: /acfg/req/disable-bsp-settings
+test-brief: |
+  This validation test suite contains a test case for the system termination
+  procedure.
+test-code: |
+  const char rtems_test_name[] = "${.:/test-suite-name}";
+
+  #define CONFIGURE_MAXIMUM_PROCESSORS 2
+
+  #define CONFIGURE_INITIAL_EXTENSIONS \
+    { .fatal = FatalExtension0 }, \
+    { .fatal = FatalExtension1 }
+
+  #define CONFIGURE_DISABLE_BSP_SETTINGS
+
+  #include "ts-default.h"
+test-description: null
+test-includes: []
+test-local-includes:
+- tc-terminate.h
+test-suite-name: Fatal
+test-target: testsuites/validation/ts-terminate.c
+type: test-suite