From 0a51cadbfd42f1c2bc868195b376156b4c4fcc34 Mon Sep 17 00:00:00 2001 From: Robbie VanVossen Date: Wed, 20 Nov 2024 12:09:52 -0500 Subject: [PATCH] Update to latest HAMR which uses queuing --- .../platform_ZCU102_Impl_Instance.aaxl2 | 484 ++++++------------ .../include/seL4_ArduPilot_ArduPilot.h | 6 +- .../src/seL4_ArduPilot_ArduPilot.c | 33 +- .../include/seL4_Firewall_Firewall.h | 10 +- .../src/seL4_Firewall_Firewall.c | 65 ++- ...velEthernetDriver_LowLevelEthernetDriver.h | 6 +- ...velEthernetDriver_LowLevelEthernetDriver.c | 30 +- .../microkit/include/sb_aadl_types.h | 31 ++ .../microkit/include/sb_event_counter.h | 5 + ..._queue_base_SW_RawEthernetMessage_Impl_1.h | 133 +++++ ...ueue_base_SW_SizedEthernetMessage_Impl_1.h | 133 +++++ .../microkit/include/sb_types.h | 10 + .../microkit/microkit.dot | 40 +- .../microkit/microkit.system | 48 +- ..._queue_base_SW_RawEthernetMessage_Impl_1.c | 117 +++++ ...ueue_base_SW_SizedEthernetMessage_Impl_1.c | 117 +++++ .../microkit/system.mk | 39 +- 17 files changed, 882 insertions(+), 425 deletions(-) create mode 100644 open-platform-models/isolate-ethernet-simple/microkit/include/sb_aadl_types.h create mode 100644 open-platform-models/isolate-ethernet-simple/microkit/include/sb_event_counter.h create mode 100644 open-platform-models/isolate-ethernet-simple/microkit/include/sb_queue_base_SW_RawEthernetMessage_Impl_1.h create mode 100644 open-platform-models/isolate-ethernet-simple/microkit/include/sb_queue_base_SW_SizedEthernetMessage_Impl_1.h create mode 100644 open-platform-models/isolate-ethernet-simple/microkit/include/sb_types.h create mode 100644 open-platform-models/isolate-ethernet-simple/microkit/src/sb_queue_base_SW_RawEthernetMessage_Impl_1.c create mode 100644 open-platform-models/isolate-ethernet-simple/microkit/src/sb_queue_base_SW_SizedEthernetMessage_Impl_1.c diff --git a/open-platform-models/isolate-ethernet-simple/aadl/instances/platform_ZCU102_Impl_Instance.aaxl2 b/open-platform-models/isolate-ethernet-simple/aadl/instances/platform_ZCU102_Impl_Instance.aaxl2 index 7f60340..72abbc1 100644 --- a/open-platform-models/isolate-ethernet-simple/aadl/instances/platform_ZCU102_Impl_Instance.aaxl2 +++ b/open-platform-models/isolate-ethernet-simple/aadl/instances/platform_ZCU102_Impl_Instance.aaxl2 @@ -63,7 +63,7 @@ - + @@ -95,7 +95,7 @@ - + @@ -127,7 +127,7 @@ - + @@ -146,7 +146,7 @@ - + @@ -155,7 +155,7 @@ - + @@ -169,7 +169,7 @@ - + @@ -178,7 +178,7 @@ - + @@ -187,21 +187,21 @@ - + - + - + @@ -240,9 +240,9 @@ - + - + @@ -281,15 +281,15 @@ - + - + - + 0 - + 0 @@ -308,7 +308,7 @@ - + @@ -340,7 +340,7 @@ - + @@ -372,7 +372,7 @@ - + @@ -404,69 +404,19 @@ - + - + - - - - - - - - - - - - + - + - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + @@ -485,7 +435,7 @@ - + @@ -494,7 +444,7 @@ - + @@ -508,7 +458,7 @@ - + @@ -517,7 +467,7 @@ - + @@ -526,21 +476,21 @@ - + - + - + @@ -579,9 +529,9 @@ - + - + @@ -620,9 +570,9 @@ - + - + @@ -661,60 +611,19 @@ - + - + - + - - - - - - - - - - - - + - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + @@ -723,33 +632,15 @@ - - - - - - - - - - - - - - - - - - - + - + - + 0 - + 0 @@ -768,7 +659,7 @@ - + @@ -800,69 +691,19 @@ - + - + - - - - - - - - - - - - - - - - - - - - - + - + - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + @@ -881,7 +722,7 @@ - + @@ -890,7 +731,7 @@ - + @@ -904,7 +745,7 @@ - + @@ -913,7 +754,7 @@ - + @@ -922,21 +763,21 @@ - + - + - + @@ -975,60 +816,19 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + - + - + - + - + @@ -1037,89 +837,60 @@ - - - - - - - - - - - - - - - - - - - + - + - + 0 - + 0 - + - + - + - + - + - + - + - + - - - - - - - - - - - - + - + - + - + @@ -1171,34 +942,91 @@ - + - + - + - + - - - - - + + + + + + + - - - - - - - - + + + + + + + + + + - - - - + + + + + + + + + + + + + + + + + + + + + + 0 + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + 0 + + + diff --git a/open-platform-models/isolate-ethernet-simple/microkit/components/seL4_ArduPilot_ArduPilot/include/seL4_ArduPilot_ArduPilot.h b/open-platform-models/isolate-ethernet-simple/microkit/components/seL4_ArduPilot_ArduPilot/include/seL4_ArduPilot_ArduPilot.h index f5c2993..812d6aa 100644 --- a/open-platform-models/isolate-ethernet-simple/microkit/components/seL4_ArduPilot_ArduPilot/include/seL4_ArduPilot_ArduPilot.h +++ b/open-platform-models/isolate-ethernet-simple/microkit/components/seL4_ArduPilot_ArduPilot/include/seL4_ArduPilot_ArduPilot.h @@ -1,7 +1,7 @@ #include #include #include -#include +#include -void getEthernetFramesRx(uint8_t *value); -void putEthernetFramesTx(uint8_t *value); +bool put_EthernetFramesTx(const base_SW_RawEthernetMessage_Impl *data); +bool get_EthernetFramesRx(base_SW_RawEthernetMessage_Impl *data); diff --git a/open-platform-models/isolate-ethernet-simple/microkit/components/seL4_ArduPilot_ArduPilot/src/seL4_ArduPilot_ArduPilot.c b/open-platform-models/isolate-ethernet-simple/microkit/components/seL4_ArduPilot_ArduPilot/src/seL4_ArduPilot_ArduPilot.c index a68d72c..83b81fb 100644 --- a/open-platform-models/isolate-ethernet-simple/microkit/components/seL4_ArduPilot_ArduPilot/src/seL4_ArduPilot_ArduPilot.c +++ b/open-platform-models/isolate-ethernet-simple/microkit/components/seL4_ArduPilot_ArduPilot/src/seL4_ArduPilot_ArduPilot.c @@ -3,26 +3,37 @@ void seL4_ArduPilot_ArduPilot_initialize(void); void seL4_ArduPilot_ArduPilot_timeTriggered(void); -volatile uint8_t *EthernetFramesRx; -volatile uint8_t *EthernetFramesTx; +volatile sb_queue_base_SW_RawEthernetMessage_Impl_1_t *EthernetFramesTx_queue_1; +volatile sb_queue_base_SW_RawEthernetMessage_Impl_1_t *EthernetFramesRx_queue_1; +sb_queue_base_SW_RawEthernetMessage_Impl_1_Recv_t EthernetFramesRx_recv_queue; #define PORT_FROM_MON 60 -void getEthernetFramesRx(uint8_t *value) { - // TODO need memmove or memcpy - for (int i = 0; i < slang_SW_RawEthernetMessage_Impl_SIZE; i++){ - value[i] = EthernetFramesRx[i]; - } +bool put_EthernetFramesTx(const base_SW_RawEthernetMessage_Impl *data) { + sb_queue_base_SW_RawEthernetMessage_Impl_1_enqueue((sb_queue_base_SW_RawEthernetMessage_Impl_1_t *) EthernetFramesTx_queue_1, (base_SW_RawEthernetMessage_Impl *) data); + + return true; } -void putEthernetFramesTx(uint8_t *value) { - // TODO need memmove or memcpy - for (int i = 0; i < slang_SW_RawEthernetMessage_Impl_SIZE; i++){ - EthernetFramesTx[i] = value[i]; +base_SW_RawEthernetMessage_Impl last_EthernetFramesRx_payload; + +bool get_EthernetFramesRx(base_SW_RawEthernetMessage_Impl *data) { + sb_event_counter_t numDropped; + base_SW_RawEthernetMessage_Impl fresh_data; + bool isFresh = false; + if (sb_queue_base_SW_RawEthernetMessage_Impl_1_dequeue((sb_queue_base_SW_RawEthernetMessage_Impl_1_Recv_t *) &EthernetFramesRx_recv_queue, &numDropped, &fresh_data)) { + last_EthernetFramesRx_payload = fresh_data; + isFresh = true; } + *data = last_EthernetFramesRx_payload; + return isFresh; } void init(void) { + sb_queue_base_SW_RawEthernetMessage_Impl_1_init((sb_queue_base_SW_RawEthernetMessage_Impl_1_t *) EthernetFramesTx_queue_1); + + sb_queue_base_SW_RawEthernetMessage_Impl_1_Recv_init(&EthernetFramesRx_recv_queue, (sb_queue_base_SW_RawEthernetMessage_Impl_1_t *) EthernetFramesRx_queue_1); + seL4_ArduPilot_ArduPilot_initialize(); } diff --git a/open-platform-models/isolate-ethernet-simple/microkit/components/seL4_Firewall_Firewall/include/seL4_Firewall_Firewall.h b/open-platform-models/isolate-ethernet-simple/microkit/components/seL4_Firewall_Firewall/include/seL4_Firewall_Firewall.h index a4f9170..26689a6 100644 --- a/open-platform-models/isolate-ethernet-simple/microkit/components/seL4_Firewall_Firewall/include/seL4_Firewall_Firewall.h +++ b/open-platform-models/isolate-ethernet-simple/microkit/components/seL4_Firewall_Firewall/include/seL4_Firewall_Firewall.h @@ -1,9 +1,9 @@ #include #include #include -#include +#include -void getEthernetFramesRxIn(uint8_t *value); -void getEthernetFramesTxIn(uint8_t *value); -void putEthernetFramesRxOut(uint8_t *value); -void putEthernetFramesTxOut(slang_SW_SizedEthernetMessage_Impl *value); +bool get_EthernetFramesTxIn(base_SW_RawEthernetMessage_Impl *data); +bool put_EthernetFramesRxOut(const base_SW_RawEthernetMessage_Impl *data); +bool put_EthernetFramesTxOut(const base_SW_SizedEthernetMessage_Impl *data); +bool get_EthernetFramesRxIn(base_SW_RawEthernetMessage_Impl *data); diff --git a/open-platform-models/isolate-ethernet-simple/microkit/components/seL4_Firewall_Firewall/src/seL4_Firewall_Firewall.c b/open-platform-models/isolate-ethernet-simple/microkit/components/seL4_Firewall_Firewall/src/seL4_Firewall_Firewall.c index d6805c6..ad553ed 100644 --- a/open-platform-models/isolate-ethernet-simple/microkit/components/seL4_Firewall_Firewall/src/seL4_Firewall_Firewall.c +++ b/open-platform-models/isolate-ethernet-simple/microkit/components/seL4_Firewall_Firewall/src/seL4_Firewall_Firewall.c @@ -3,39 +3,64 @@ void seL4_Firewall_Firewall_initialize(void); void seL4_Firewall_Firewall_timeTriggered(void); -volatile uint8_t *EthernetFramesRxIn; -volatile uint8_t *EthernetFramesTxIn; -volatile uint8_t *EthernetFramesRxOut; -volatile slang_SW_SizedEthernetMessage_Impl *EthernetFramesTxOut; +volatile sb_queue_base_SW_RawEthernetMessage_Impl_1_t *EthernetFramesTxIn_queue_1; +sb_queue_base_SW_RawEthernetMessage_Impl_1_Recv_t EthernetFramesTxIn_recv_queue; +volatile sb_queue_base_SW_RawEthernetMessage_Impl_1_t *EthernetFramesRxOut_queue_1; +volatile sb_queue_base_SW_SizedEthernetMessage_Impl_1_t *EthernetFramesTxOut_queue_1; +volatile sb_queue_base_SW_RawEthernetMessage_Impl_1_t *EthernetFramesRxIn_queue_1; +sb_queue_base_SW_RawEthernetMessage_Impl_1_Recv_t EthernetFramesRxIn_recv_queue; #define PORT_FROM_MON 58 -void getEthernetFramesRxIn(uint8_t *value) { - // TODO need memmove or memcpy - for (int i = 0; i < slang_SW_RawEthernetMessage_Impl_SIZE; i++){ - value[i] = EthernetFramesRxIn[i]; +base_SW_RawEthernetMessage_Impl last_EthernetFramesTxIn_payload; + +bool get_EthernetFramesTxIn(base_SW_RawEthernetMessage_Impl *data) { + sb_event_counter_t numDropped; + base_SW_RawEthernetMessage_Impl fresh_data; + bool isFresh = false; + if (sb_queue_base_SW_RawEthernetMessage_Impl_1_dequeue((sb_queue_base_SW_RawEthernetMessage_Impl_1_Recv_t *) &EthernetFramesTxIn_recv_queue, &numDropped, &fresh_data)) { + last_EthernetFramesTxIn_payload = fresh_data; + isFresh = true; } + *data = last_EthernetFramesTxIn_payload; + return isFresh; } -void getEthernetFramesTxIn(uint8_t *value) { - // TODO need memmove or memcpy - for (int i = 0; i < slang_SW_RawEthernetMessage_Impl_SIZE; i++){ - value[i] = EthernetFramesTxIn[i]; - } +bool put_EthernetFramesRxOut(const base_SW_RawEthernetMessage_Impl *data) { + sb_queue_base_SW_RawEthernetMessage_Impl_1_enqueue((sb_queue_base_SW_RawEthernetMessage_Impl_1_t *) EthernetFramesRxOut_queue_1, (base_SW_RawEthernetMessage_Impl *) data); + + return true; } -void putEthernetFramesRxOut(uint8_t *value) { - // TODO need memmove or memcpy - for (int i = 0; i < slang_SW_RawEthernetMessage_Impl_SIZE; i++){ - EthernetFramesRxOut[i] = value[i]; - } +bool put_EthernetFramesTxOut(const base_SW_SizedEthernetMessage_Impl *data) { + sb_queue_base_SW_SizedEthernetMessage_Impl_1_enqueue((sb_queue_base_SW_SizedEthernetMessage_Impl_1_t *) EthernetFramesTxOut_queue_1, (base_SW_SizedEthernetMessage_Impl *) data); + + return true; } -void putEthernetFramesTxOut(slang_SW_SizedEthernetMessage_Impl *value) { - *EthernetFramesTxOut = *value; +base_SW_RawEthernetMessage_Impl last_EthernetFramesRxIn_payload; + +bool get_EthernetFramesRxIn(base_SW_RawEthernetMessage_Impl *data) { + sb_event_counter_t numDropped; + base_SW_RawEthernetMessage_Impl fresh_data; + bool isFresh = false; + if (sb_queue_base_SW_RawEthernetMessage_Impl_1_dequeue((sb_queue_base_SW_RawEthernetMessage_Impl_1_Recv_t *) &EthernetFramesRxIn_recv_queue, &numDropped, &fresh_data)) { + last_EthernetFramesRxIn_payload = fresh_data; + isFresh = true; + } + *data = last_EthernetFramesRxIn_payload; + return isFresh; } void init(void) { + sb_queue_base_SW_RawEthernetMessage_Impl_1_Recv_init(&EthernetFramesTxIn_recv_queue, (sb_queue_base_SW_RawEthernetMessage_Impl_1_t *) EthernetFramesTxIn_queue_1); + + sb_queue_base_SW_RawEthernetMessage_Impl_1_init((sb_queue_base_SW_RawEthernetMessage_Impl_1_t *) EthernetFramesRxOut_queue_1); + + sb_queue_base_SW_SizedEthernetMessage_Impl_1_init((sb_queue_base_SW_SizedEthernetMessage_Impl_1_t *) EthernetFramesTxOut_queue_1); + + sb_queue_base_SW_RawEthernetMessage_Impl_1_Recv_init(&EthernetFramesRxIn_recv_queue, (sb_queue_base_SW_RawEthernetMessage_Impl_1_t *) EthernetFramesRxIn_queue_1); + seL4_Firewall_Firewall_initialize(); } diff --git a/open-platform-models/isolate-ethernet-simple/microkit/components/seL4_LowLevelEthernetDriver_LowLevelEthernetDriver/include/seL4_LowLevelEthernetDriver_LowLevelEthernetDriver.h b/open-platform-models/isolate-ethernet-simple/microkit/components/seL4_LowLevelEthernetDriver_LowLevelEthernetDriver/include/seL4_LowLevelEthernetDriver_LowLevelEthernetDriver.h index 634e4e4..fc46ec7 100644 --- a/open-platform-models/isolate-ethernet-simple/microkit/components/seL4_LowLevelEthernetDriver_LowLevelEthernetDriver/include/seL4_LowLevelEthernetDriver_LowLevelEthernetDriver.h +++ b/open-platform-models/isolate-ethernet-simple/microkit/components/seL4_LowLevelEthernetDriver_LowLevelEthernetDriver/include/seL4_LowLevelEthernetDriver_LowLevelEthernetDriver.h @@ -1,7 +1,7 @@ #include #include #include -#include +#include -void putEthernetFramesRx(uint8_t *value); -void getEthernetFramesTx(slang_SW_SizedEthernetMessage_Impl *value); +bool get_EthernetFramesTx(base_SW_SizedEthernetMessage_Impl *data); +bool put_EthernetFramesRx(const base_SW_RawEthernetMessage_Impl *data); diff --git a/open-platform-models/isolate-ethernet-simple/microkit/components/seL4_LowLevelEthernetDriver_LowLevelEthernetDriver/src/seL4_LowLevelEthernetDriver_LowLevelEthernetDriver.c b/open-platform-models/isolate-ethernet-simple/microkit/components/seL4_LowLevelEthernetDriver_LowLevelEthernetDriver/src/seL4_LowLevelEthernetDriver_LowLevelEthernetDriver.c index 4407425..cf61fbc 100644 --- a/open-platform-models/isolate-ethernet-simple/microkit/components/seL4_LowLevelEthernetDriver_LowLevelEthernetDriver/src/seL4_LowLevelEthernetDriver_LowLevelEthernetDriver.c +++ b/open-platform-models/isolate-ethernet-simple/microkit/components/seL4_LowLevelEthernetDriver_LowLevelEthernetDriver/src/seL4_LowLevelEthernetDriver_LowLevelEthernetDriver.c @@ -3,23 +3,37 @@ void seL4_LowLevelEthernetDriver_LowLevelEthernetDriver_initialize(void); void seL4_LowLevelEthernetDriver_LowLevelEthernetDriver_timeTriggered(void); -volatile uint8_t *EthernetFramesRx; -volatile slang_SW_SizedEthernetMessage_Impl *EthernetFramesTx; +volatile sb_queue_base_SW_SizedEthernetMessage_Impl_1_t *EthernetFramesTx_queue_1; +sb_queue_base_SW_SizedEthernetMessage_Impl_1_Recv_t EthernetFramesTx_recv_queue; +volatile sb_queue_base_SW_RawEthernetMessage_Impl_1_t *EthernetFramesRx_queue_1; #define PORT_FROM_MON 56 -void putEthernetFramesRx(uint8_t *value) { - // TODO need memmove or memcpy - for (int i = 0; i < slang_SW_RawEthernetMessage_Impl_SIZE; i++){ - EthernetFramesRx[i] = value[i]; +base_SW_SizedEthernetMessage_Impl last_EthernetFramesTx_payload; + +bool get_EthernetFramesTx(base_SW_SizedEthernetMessage_Impl *data) { + sb_event_counter_t numDropped; + base_SW_SizedEthernetMessage_Impl fresh_data; + bool isFresh = false; + if (sb_queue_base_SW_SizedEthernetMessage_Impl_1_dequeue((sb_queue_base_SW_SizedEthernetMessage_Impl_1_Recv_t *) &EthernetFramesTx_recv_queue, &numDropped, &fresh_data)) { + last_EthernetFramesTx_payload = fresh_data; + isFresh = true; } + *data = last_EthernetFramesTx_payload; + return isFresh; } -void getEthernetFramesTx(slang_SW_SizedEthernetMessage_Impl *value) { - *value = *EthernetFramesTx; +bool put_EthernetFramesRx(const base_SW_RawEthernetMessage_Impl *data) { + sb_queue_base_SW_RawEthernetMessage_Impl_1_enqueue((sb_queue_base_SW_RawEthernetMessage_Impl_1_t *) EthernetFramesRx_queue_1, (base_SW_RawEthernetMessage_Impl *) data); + + return true; } void init(void) { + sb_queue_base_SW_SizedEthernetMessage_Impl_1_Recv_init(&EthernetFramesTx_recv_queue, (sb_queue_base_SW_SizedEthernetMessage_Impl_1_t *) EthernetFramesTx_queue_1); + + sb_queue_base_SW_RawEthernetMessage_Impl_1_init((sb_queue_base_SW_RawEthernetMessage_Impl_1_t *) EthernetFramesRx_queue_1); + seL4_LowLevelEthernetDriver_LowLevelEthernetDriver_initialize(); } diff --git a/open-platform-models/isolate-ethernet-simple/microkit/include/sb_aadl_types.h b/open-platform-models/isolate-ethernet-simple/microkit/include/sb_aadl_types.h new file mode 100644 index 0000000..3e705c0 --- /dev/null +++ b/open-platform-models/isolate-ethernet-simple/microkit/include/sb_aadl_types.h @@ -0,0 +1,31 @@ +#ifndef SB_AADL_TYPES_H +#define SB_AADL_TYPES_H + +#include + +typedef struct base_SW_SizedEthernetMessage_Impl base_SW_SizedEthernetMessage_Impl; + +#define base_SW_RawEthernetMessage_Impl_SIZE 1600 + +typedef uint8_t base_SW_RawEthernetMessage_Impl [base_SW_RawEthernetMessage_Impl_SIZE]; + +typedef + struct base_SW_RawEthernetMessage_Impl_container{ + base_SW_RawEthernetMessage_Impl f; + } base_SW_RawEthernetMessage_Impl_container; + +#define base_SW_RawEthernetMessage_SIZE 1600 + +typedef uint8_t base_SW_RawEthernetMessage [base_SW_RawEthernetMessage_SIZE]; + +typedef + struct base_SW_RawEthernetMessage_container{ + base_SW_RawEthernetMessage f; + } base_SW_RawEthernetMessage_container; + +struct base_SW_SizedEthernetMessage_Impl { + message; + size; +}; + +#endif diff --git a/open-platform-models/isolate-ethernet-simple/microkit/include/sb_event_counter.h b/open-platform-models/isolate-ethernet-simple/microkit/include/sb_event_counter.h new file mode 100644 index 0000000..8972e45 --- /dev/null +++ b/open-platform-models/isolate-ethernet-simple/microkit/include/sb_event_counter.h @@ -0,0 +1,5 @@ +#pragma once + +#include + +typedef _Atomic uintmax_t sb_event_counter_t; diff --git a/open-platform-models/isolate-ethernet-simple/microkit/include/sb_queue_base_SW_RawEthernetMessage_Impl_1.h b/open-platform-models/isolate-ethernet-simple/microkit/include/sb_queue_base_SW_RawEthernetMessage_Impl_1.h new file mode 100644 index 0000000..ed23c59 --- /dev/null +++ b/open-platform-models/isolate-ethernet-simple/microkit/include/sb_queue_base_SW_RawEthernetMessage_Impl_1.h @@ -0,0 +1,133 @@ +/* + * Copyright 2017, Data61 + * Commonwealth Scientific and Industrial Research Organisation (CSIRO) + * ABN 41 687 119 230. + * + * Copyright 2019 Adventium Labs + * Modifications made to original + * + * This software may be distributed and modified according to the terms of + * the BSD 2-Clause license. Note that NO WARRANTY is provided. + * See "LICENSE_BSD2.txt" for details. + * + * @TAG(DATA61_Adventium_BSD) + */ + +// Single sender multiple receiver Queue implementation for AADL +// Ports. Every receiver receives the sent data (ie broadcast). The queue +// operations are all non-blocking. The sender enqueue always succeeds. A +// receiver dequeue can fail and drop data if the sender writes while the +// receiver is reading. This situation is detected unless the sender gets +// ahead of a receiver by more than COUNTER_MAX. Since COUNTER_MAX is typically +// 2^64 (see sb_event_counter.h), this is extremely unlikely. If it does happen the +// only adverse effect is that the receiver will not detect all dropped +// elements. + +#pragma once + +#include +#include +#include + +// Queue size must be an integer factor of the size for sb_event_counter_t (an unsigned +// integer type). Since we are using standard C unsigned integers for the +// counter, picking a queue size that is a power of 2 is a good choice. We +// could alternatively set the size of our counter to the largest possible +// multiple of queue size. But then we would need to do our own modulo +// operations on the counter rather than depending on c's unsigned integer +// operations. +// +// Note: One cell in the queue is always considered dirty. Its the next +// element to be written. Thus the queue can only contain +// SB_QUEUE_BASE_SW_RAWETHERNETMESSAGE_IMPL_1_SIZE-1 elements. +#define SB_QUEUE_BASE_SW_RAWETHERNETMESSAGE_IMPL_1_SIZE 2 + +// This is the type of the seL4 dataport (shared memory) that is shared by the +// sender and all receivers. This type is referenced in the sender and receiver +// component definition files. The seL4 runtime creates an +// instance of this struct. +typedef struct sb_queue_base_SW_RawEthernetMessage_Impl_1 { + // Number of elements enqueued by the sender. The implementation depends + // on C's standard module behaviour for unsigned integers. The counter never + // overflows. It just wraps modulo the size of the counter type. The counter + // is typically very large (see sb_event_counter.h), so this should happen very + // infrequently. Depending in C to initialize this to zero. + _Atomic sb_event_counter_t numSent; + + // Queue of elements of type base_SW_RawEthernetMessage_Impl + // (see sb_types.h) implemented as a ring buffer. + // No initialization necessary. + base_SW_RawEthernetMessage_Impl elt[SB_QUEUE_BASE_SW_RAWETHERNETMESSAGE_IMPL_1_SIZE]; + +} sb_queue_base_SW_RawEthernetMessage_Impl_1_t; + +//------------------------------------------------------------------------------ +// Sender API +// +// Could split this into separate header and source file since only sender +// code needs this. + +// Initialize the queue. Sender must call this exactly once before any calls to queue_enqueue(); +void sb_queue_base_SW_RawEthernetMessage_Impl_1_init(sb_queue_base_SW_RawEthernetMessage_Impl_1_t *queue); + +// Enqueue data. This always succeeds and never blocks. Data is copied. +void sb_queue_base_SW_RawEthernetMessage_Impl_1_enqueue( + sb_queue_base_SW_RawEthernetMessage_Impl_1_t *queue, + base_SW_RawEthernetMessage_Impl *data); + +//------------------------------------------------------------------------------ +// Receiver API +// +// Could split this into separate header and source file since only receiver +// code needs this. + +// Each receiver needs to create an instance of this. +typedef struct sb_queue_base_SW_RawEthernetMessage_Impl_1_Recv { + // Number of elements dequeued (or dropped) by a receiver. The implementation + // depends on C's standard module behaviour for unsigned integers. The + // counter never overflows. It just wraps modulo the size of the counter + // type. The counter is typically very large (see counter.h), so this should + // happen very infrequently. + sb_event_counter_t numRecv; + + // Pointer to the actual queue. This is the seL4 dataport (shared memory) + // that is shared by the sender and all receivers. + sb_queue_base_SW_RawEthernetMessage_Impl_1_t *queue; + +} sb_queue_base_SW_RawEthernetMessage_Impl_1_Recv_t; + +// Each receiver must call this exactly once before any calls to other queue +// API functions. +void sb_queue_base_SW_RawEthernetMessage_Impl_1_Recv_init( + sb_queue_base_SW_RawEthernetMessage_Impl_1_Recv_t *recvQueue, + sb_queue_base_SW_RawEthernetMessage_Impl_1_t *queue); + +// Dequeue data. Never blocks but can fail if the sender writes at same +// time. + +// When successful returns true. The dequeued data will be copied to +// *data. *numDropped will contain the number of elements that were dropped +// since the last call to queue_dequeue(). +// +// When queue is empty, returns false and *numDropped is zero. *data is left in +// unspecified state. +// +// When dequeue fails due to possible write of data being read, returns false +// and *numDropped will be >= 1 specifying the number of elements that were +// dropped since the last call to sb_queue_base_SW_RawEthernetMessage_Impl_1_dequeue(). *data is left in +// unspecified state. +// +// If the sender ever gets ahead of a receiver by more than COUNTER_MAX, +// sb_queue_base_SW_RawEthernetMessage_Impl_1_dequeue will fail to count a multiple of COUNTER_MAX in +// numDropped. Since COUNTER_MAX is very large (typically on the order of 2^64, +// see sb_event_counter.h), this is very unlikely. If the sender is ever this far +// ahead of a receiver the system is probably in a very bad state. +bool sb_queue_base_SW_RawEthernetMessage_Impl_1_dequeue( + sb_queue_base_SW_RawEthernetMessage_Impl_1_Recv_t *recvQueue, + sb_event_counter_t *numDropped, + base_SW_RawEthernetMessage_Impl *data); + +// Is queue empty? If the queue is not empty, it will stay that way until the +// receiver dequeues all data. If the queue is empty you can make no +// assumptions about how long it will stay empty. +bool sb_queue_base_SW_RawEthernetMessage_Impl_1_is_empty(sb_queue_base_SW_RawEthernetMessage_Impl_1_Recv_t *recvQueue); diff --git a/open-platform-models/isolate-ethernet-simple/microkit/include/sb_queue_base_SW_SizedEthernetMessage_Impl_1.h b/open-platform-models/isolate-ethernet-simple/microkit/include/sb_queue_base_SW_SizedEthernetMessage_Impl_1.h new file mode 100644 index 0000000..ff25d1b --- /dev/null +++ b/open-platform-models/isolate-ethernet-simple/microkit/include/sb_queue_base_SW_SizedEthernetMessage_Impl_1.h @@ -0,0 +1,133 @@ +/* + * Copyright 2017, Data61 + * Commonwealth Scientific and Industrial Research Organisation (CSIRO) + * ABN 41 687 119 230. + * + * Copyright 2019 Adventium Labs + * Modifications made to original + * + * This software may be distributed and modified according to the terms of + * the BSD 2-Clause license. Note that NO WARRANTY is provided. + * See "LICENSE_BSD2.txt" for details. + * + * @TAG(DATA61_Adventium_BSD) + */ + +// Single sender multiple receiver Queue implementation for AADL +// Ports. Every receiver receives the sent data (ie broadcast). The queue +// operations are all non-blocking. The sender enqueue always succeeds. A +// receiver dequeue can fail and drop data if the sender writes while the +// receiver is reading. This situation is detected unless the sender gets +// ahead of a receiver by more than COUNTER_MAX. Since COUNTER_MAX is typically +// 2^64 (see sb_event_counter.h), this is extremely unlikely. If it does happen the +// only adverse effect is that the receiver will not detect all dropped +// elements. + +#pragma once + +#include +#include +#include + +// Queue size must be an integer factor of the size for sb_event_counter_t (an unsigned +// integer type). Since we are using standard C unsigned integers for the +// counter, picking a queue size that is a power of 2 is a good choice. We +// could alternatively set the size of our counter to the largest possible +// multiple of queue size. But then we would need to do our own modulo +// operations on the counter rather than depending on c's unsigned integer +// operations. +// +// Note: One cell in the queue is always considered dirty. Its the next +// element to be written. Thus the queue can only contain +// SB_QUEUE_BASE_SW_SIZEDETHERNETMESSAGE_IMPL_1_SIZE-1 elements. +#define SB_QUEUE_BASE_SW_SIZEDETHERNETMESSAGE_IMPL_1_SIZE 2 + +// This is the type of the seL4 dataport (shared memory) that is shared by the +// sender and all receivers. This type is referenced in the sender and receiver +// component definition files. The seL4 runtime creates an +// instance of this struct. +typedef struct sb_queue_base_SW_SizedEthernetMessage_Impl_1 { + // Number of elements enqueued by the sender. The implementation depends + // on C's standard module behaviour for unsigned integers. The counter never + // overflows. It just wraps modulo the size of the counter type. The counter + // is typically very large (see sb_event_counter.h), so this should happen very + // infrequently. Depending in C to initialize this to zero. + _Atomic sb_event_counter_t numSent; + + // Queue of elements of type base_SW_SizedEthernetMessage_Impl + // (see sb_types.h) implemented as a ring buffer. + // No initialization necessary. + base_SW_SizedEthernetMessage_Impl elt[SB_QUEUE_BASE_SW_SIZEDETHERNETMESSAGE_IMPL_1_SIZE]; + +} sb_queue_base_SW_SizedEthernetMessage_Impl_1_t; + +//------------------------------------------------------------------------------ +// Sender API +// +// Could split this into separate header and source file since only sender +// code needs this. + +// Initialize the queue. Sender must call this exactly once before any calls to queue_enqueue(); +void sb_queue_base_SW_SizedEthernetMessage_Impl_1_init(sb_queue_base_SW_SizedEthernetMessage_Impl_1_t *queue); + +// Enqueue data. This always succeeds and never blocks. Data is copied. +void sb_queue_base_SW_SizedEthernetMessage_Impl_1_enqueue( + sb_queue_base_SW_SizedEthernetMessage_Impl_1_t *queue, + base_SW_SizedEthernetMessage_Impl *data); + +//------------------------------------------------------------------------------ +// Receiver API +// +// Could split this into separate header and source file since only receiver +// code needs this. + +// Each receiver needs to create an instance of this. +typedef struct sb_queue_base_SW_SizedEthernetMessage_Impl_1_Recv { + // Number of elements dequeued (or dropped) by a receiver. The implementation + // depends on C's standard module behaviour for unsigned integers. The + // counter never overflows. It just wraps modulo the size of the counter + // type. The counter is typically very large (see counter.h), so this should + // happen very infrequently. + sb_event_counter_t numRecv; + + // Pointer to the actual queue. This is the seL4 dataport (shared memory) + // that is shared by the sender and all receivers. + sb_queue_base_SW_SizedEthernetMessage_Impl_1_t *queue; + +} sb_queue_base_SW_SizedEthernetMessage_Impl_1_Recv_t; + +// Each receiver must call this exactly once before any calls to other queue +// API functions. +void sb_queue_base_SW_SizedEthernetMessage_Impl_1_Recv_init( + sb_queue_base_SW_SizedEthernetMessage_Impl_1_Recv_t *recvQueue, + sb_queue_base_SW_SizedEthernetMessage_Impl_1_t *queue); + +// Dequeue data. Never blocks but can fail if the sender writes at same +// time. + +// When successful returns true. The dequeued data will be copied to +// *data. *numDropped will contain the number of elements that were dropped +// since the last call to queue_dequeue(). +// +// When queue is empty, returns false and *numDropped is zero. *data is left in +// unspecified state. +// +// When dequeue fails due to possible write of data being read, returns false +// and *numDropped will be >= 1 specifying the number of elements that were +// dropped since the last call to sb_queue_base_SW_SizedEthernetMessage_Impl_1_dequeue(). *data is left in +// unspecified state. +// +// If the sender ever gets ahead of a receiver by more than COUNTER_MAX, +// sb_queue_base_SW_SizedEthernetMessage_Impl_1_dequeue will fail to count a multiple of COUNTER_MAX in +// numDropped. Since COUNTER_MAX is very large (typically on the order of 2^64, +// see sb_event_counter.h), this is very unlikely. If the sender is ever this far +// ahead of a receiver the system is probably in a very bad state. +bool sb_queue_base_SW_SizedEthernetMessage_Impl_1_dequeue( + sb_queue_base_SW_SizedEthernetMessage_Impl_1_Recv_t *recvQueue, + sb_event_counter_t *numDropped, + base_SW_SizedEthernetMessage_Impl *data); + +// Is queue empty? If the queue is not empty, it will stay that way until the +// receiver dequeues all data. If the queue is empty you can make no +// assumptions about how long it will stay empty. +bool sb_queue_base_SW_SizedEthernetMessage_Impl_1_is_empty(sb_queue_base_SW_SizedEthernetMessage_Impl_1_Recv_t *recvQueue); diff --git a/open-platform-models/isolate-ethernet-simple/microkit/include/sb_types.h b/open-platform-models/isolate-ethernet-simple/microkit/include/sb_types.h new file mode 100644 index 0000000..61c36a3 --- /dev/null +++ b/open-platform-models/isolate-ethernet-simple/microkit/include/sb_types.h @@ -0,0 +1,10 @@ +#ifndef SB_TYPES_H +#define SB_TYPES_H + +#include +#include +#include +#include +#include + +#endif \ No newline at end of file diff --git a/open-platform-models/isolate-ethernet-simple/microkit/microkit.dot b/open-platform-models/isolate-ethernet-simple/microkit/microkit.dot index c3eaad9..b99e5c9 100644 --- a/open-platform-models/isolate-ethernet-simple/microkit/microkit.dot +++ b/open-platform-models/isolate-ethernet-simple/microkit/microkit.dot @@ -12,8 +12,8 @@ digraph microkit { label = "seL4_ArduPilot_ArduPilot"; seL4_ArduPilot_ArduPilot_INVIS [label="", style=invis, width=.5, height=.5, fixedsize=true] - pd_seL4_ArduPilot_ArduPilot_EthernetFramesRx [label=EthernetFramesRx]; - pd_seL4_ArduPilot_ArduPilot_EthernetFramesTx [label=EthernetFramesTx]; + pd_seL4_ArduPilot_ArduPilot_EthernetFramesTx_queue_1 [label=EthernetFramesTx_queue_1]; + pd_seL4_ArduPilot_ArduPilot_EthernetFramesRx_queue_1 [label=EthernetFramesRx_queue_1]; } } @@ -27,10 +27,10 @@ digraph microkit { label = "seL4_Firewall_Firewall"; seL4_Firewall_Firewall_INVIS [label="", style=invis, width=.5, height=.5, fixedsize=true] - pd_seL4_Firewall_Firewall_EthernetFramesRxIn [label=EthernetFramesRxIn]; - pd_seL4_Firewall_Firewall_EthernetFramesTxIn [label=EthernetFramesTxIn]; - pd_seL4_Firewall_Firewall_EthernetFramesRxOut [label=EthernetFramesRxOut]; - pd_seL4_Firewall_Firewall_EthernetFramesTxOut [label=EthernetFramesTxOut]; + pd_seL4_Firewall_Firewall_EthernetFramesTxIn_queue_1 [label=EthernetFramesTxIn_queue_1]; + pd_seL4_Firewall_Firewall_EthernetFramesRxOut_queue_1 [label=EthernetFramesRxOut_queue_1]; + pd_seL4_Firewall_Firewall_EthernetFramesTxOut_queue_1 [label=EthernetFramesTxOut_queue_1]; + pd_seL4_Firewall_Firewall_EthernetFramesRxIn_queue_1 [label=EthernetFramesRxIn_queue_1]; } } @@ -44,8 +44,8 @@ digraph microkit { label = "seL4_LowLevelEthernetDriver_LowLevelEthernetDriver"; seL4_LowLevelEthernetDriver_LowLevelEthernetDriver_INVIS [label="", style=invis, width=.5, height=.5, fixedsize=true] - pd_seL4_LowLevelEthernetDriver_LowLevelEthernetDriver_EthernetFramesRx [label=EthernetFramesRx]; - pd_seL4_LowLevelEthernetDriver_LowLevelEthernetDriver_EthernetFramesTx [label=EthernetFramesTx]; + pd_seL4_LowLevelEthernetDriver_LowLevelEthernetDriver_EthernetFramesTx_queue_1 [label=EthernetFramesTx_queue_1]; + pd_seL4_LowLevelEthernetDriver_LowLevelEthernetDriver_EthernetFramesRx_queue_1 [label=EthernetFramesRx_queue_1]; } } @@ -57,13 +57,13 @@ digraph microkit { } // memory regions - seL4_Firewall_Firewall_EthernetFramesRxOut; + ZCU102_Impl_Instance_seL4_ArduPilot_ArduPilot_EthernetFramesTx_1_Memory_Region; - seL4_ArduPilot_ArduPilot_EthernetFramesTx; + ZCU102_Impl_Instance_seL4_Firewall_Firewall_EthernetFramesRxOut_1_Memory_Region; - seL4_LowLevelEthernetDriver_LowLevelEthernetDriver_EthernetFramesRx; + ZCU102_Impl_Instance_seL4_Firewall_Firewall_EthernetFramesTxOut_1_Memory_Region; - seL4_Firewall_Firewall_EthernetFramesTxOut; + ZCU102_Impl_Instance_seL4_LowLevelEthernetDriver_LowLevelEthernetDriver_EthernetFramesRx_1_Memory_Region; // channels pacer_INVIS -> seL4_ArduPilot_ArduPilot_MON_INVIS [lhead=cluster_seL4_ArduPilot_ArduPilot_MON, minlen=2, dir=both]; @@ -74,12 +74,12 @@ digraph microkit { seL4_LowLevelEthernetDriver_LowLevelEthernetDriver_MON_INVIS -> seL4_LowLevelEthernetDriver_LowLevelEthernetDriver_INVIS [lhead=cluster_seL4_LowLevelEthernetDriver_LowLevelEthernetDriver, minlen=2, dir=both]; // shared memory mappings - pd_seL4_ArduPilot_ArduPilot_EthernetFramesRx -> seL4_Firewall_Firewall_EthernetFramesRxOut [dir=back, style=dashed]; - pd_seL4_ArduPilot_ArduPilot_EthernetFramesTx -> seL4_ArduPilot_ArduPilot_EthernetFramesTx [dir=both, style=dashed]; - pd_seL4_Firewall_Firewall_EthernetFramesRxIn -> seL4_LowLevelEthernetDriver_LowLevelEthernetDriver_EthernetFramesRx [dir=back, style=dashed]; - pd_seL4_Firewall_Firewall_EthernetFramesTxIn -> seL4_ArduPilot_ArduPilot_EthernetFramesTx [dir=back, style=dashed]; - pd_seL4_Firewall_Firewall_EthernetFramesRxOut -> seL4_Firewall_Firewall_EthernetFramesRxOut [dir=both, style=dashed]; - pd_seL4_Firewall_Firewall_EthernetFramesTxOut -> seL4_Firewall_Firewall_EthernetFramesTxOut [dir=both, style=dashed]; - pd_seL4_LowLevelEthernetDriver_LowLevelEthernetDriver_EthernetFramesRx -> seL4_LowLevelEthernetDriver_LowLevelEthernetDriver_EthernetFramesRx [dir=both, style=dashed]; - pd_seL4_LowLevelEthernetDriver_LowLevelEthernetDriver_EthernetFramesTx -> seL4_Firewall_Firewall_EthernetFramesTxOut [dir=back, style=dashed]; + pd_seL4_ArduPilot_ArduPilot_EthernetFramesTx_queue_1 -> ZCU102_Impl_Instance_seL4_ArduPilot_ArduPilot_EthernetFramesTx_1_Memory_Region [dir=both, style=dashed]; + pd_seL4_ArduPilot_ArduPilot_EthernetFramesRx_queue_1 -> ZCU102_Impl_Instance_seL4_Firewall_Firewall_EthernetFramesRxOut_1_Memory_Region [dir=back, style=dashed]; + pd_seL4_Firewall_Firewall_EthernetFramesTxIn_queue_1 -> ZCU102_Impl_Instance_seL4_ArduPilot_ArduPilot_EthernetFramesTx_1_Memory_Region [dir=back, style=dashed]; + pd_seL4_Firewall_Firewall_EthernetFramesRxOut_queue_1 -> ZCU102_Impl_Instance_seL4_Firewall_Firewall_EthernetFramesRxOut_1_Memory_Region [dir=both, style=dashed]; + pd_seL4_Firewall_Firewall_EthernetFramesTxOut_queue_1 -> ZCU102_Impl_Instance_seL4_Firewall_Firewall_EthernetFramesTxOut_1_Memory_Region [dir=both, style=dashed]; + pd_seL4_Firewall_Firewall_EthernetFramesRxIn_queue_1 -> ZCU102_Impl_Instance_seL4_LowLevelEthernetDriver_LowLevelEthernetDriver_EthernetFramesRx_1_Memory_Region [dir=back, style=dashed]; + pd_seL4_LowLevelEthernetDriver_LowLevelEthernetDriver_EthernetFramesTx_queue_1 -> ZCU102_Impl_Instance_seL4_Firewall_Firewall_EthernetFramesTxOut_1_Memory_Region [dir=back, style=dashed]; + pd_seL4_LowLevelEthernetDriver_LowLevelEthernetDriver_EthernetFramesRx_queue_1 -> ZCU102_Impl_Instance_seL4_LowLevelEthernetDriver_LowLevelEthernetDriver_EthernetFramesRx_1_Memory_Region [dir=both, style=dashed]; } \ No newline at end of file diff --git a/open-platform-models/isolate-ethernet-simple/microkit/microkit.system b/open-platform-models/isolate-ethernet-simple/microkit/microkit.system index 03a59c8..289ca7a 100644 --- a/open-platform-models/isolate-ethernet-simple/microkit/microkit.system +++ b/open-platform-models/isolate-ethernet-simple/microkit/microkit.system @@ -12,8 +12,14 @@ - - + + @@ -21,10 +27,22 @@ - - - - + + + + @@ -32,8 +50,14 @@ - - + + @@ -43,13 +67,13 @@ - + - + - + - + diff --git a/open-platform-models/isolate-ethernet-simple/microkit/src/sb_queue_base_SW_RawEthernetMessage_Impl_1.c b/open-platform-models/isolate-ethernet-simple/microkit/src/sb_queue_base_SW_RawEthernetMessage_Impl_1.c new file mode 100644 index 0000000..bc5aab5 --- /dev/null +++ b/open-platform-models/isolate-ethernet-simple/microkit/src/sb_queue_base_SW_RawEthernetMessage_Impl_1.c @@ -0,0 +1,117 @@ +/* + * Copyright 2017, Data61 + * Commonwealth Scientific and Industrial Research Organisation (CSIRO) + * ABN 41 687 119 230. + * + * Copyright 2019 Adventium Labs + * Modifications made to original + * + * This software may be distributed and modified according to the terms of + * the BSD 2-Clause license. Note that NO WARRANTY is provided. + * See "LICENSE_BSD2.txt" for details. + * + * @TAG(DATA61_Adventium_BSD) + */ + +#include +#include +#include + +//------------------------------------------------------------------------------ +// Sender API +// +// See sb_queue_base_SW_RawEthernetMessage_Impl_1.h for API documentation. Only implementation details are documented here. + +void sb_queue_base_SW_RawEthernetMessage_Impl_1_init(sb_queue_base_SW_RawEthernetMessage_Impl_1_t *queue) { + // NOOP for now. C's struct initialization is sufficient. If we ever do need + // initialization logic, we may also need to synchronize with receiver + // startup. +} + +void sb_queue_base_SW_RawEthernetMessage_Impl_1_enqueue( + sb_queue_base_SW_RawEthernetMessage_Impl_1_t *queue, + base_SW_RawEthernetMessage_Impl *data) { + + // Simple ring with one dirty element that will be written next. Only one + // writer, so no need for any synchronization. + // elt[queue->numSent % SB_QUEUE_BASE_SW_RAWETHERNETMESSAGE_IMPL_1_SIZE] + // is always considered dirty. So do not advance queue->NumSent + // till AFTER data is copied. + + size_t index = queue->numSent % SB_QUEUE_BASE_SW_RAWETHERNETMESSAGE_IMPL_1_SIZE; + + queue->elt[index] = *data; // Copy data into queue + + // Release memory fence - ensure that data write above completes BEFORE we advance queue->numSent + __atomic_thread_fence(__ATOMIC_RELEASE); + + ++(queue->numSent); +} + +//------------------------------------------------------------------------------ +// Receiver API +// +// See sb_queue_base_SW_RawEthernetMessage_Impl_1.h for API documentation. Only implementation details are documented here. + +void sb_queue_base_SW_RawEthernetMessage_Impl_1_Recv_init( + sb_queue_base_SW_RawEthernetMessage_Impl_1_Recv_t *recvQueue, + sb_queue_base_SW_RawEthernetMessage_Impl_1_t *queue) { + + recvQueue->numRecv = 0; + recvQueue->queue = queue; +} + +bool sb_queue_base_SW_RawEthernetMessage_Impl_1_dequeue( + sb_queue_base_SW_RawEthernetMessage_Impl_1_Recv_t *recvQueue, + sb_event_counter_t *numDropped, + base_SW_RawEthernetMessage_Impl *data) { + + sb_event_counter_t *numRecv = &recvQueue->numRecv; + sb_queue_base_SW_RawEthernetMessage_Impl_1_t *queue = recvQueue->queue; + + // Get a copy of numSent so we can see if it changes during read + sb_event_counter_t numSent = queue->numSent; + + // Acquire memory fence - ensure read of queue->numSent BEFORE reading data + __atomic_thread_fence(__ATOMIC_ACQUIRE); + + // How many new elements have been sent? Since we are using unsigned + // integers, this correctly computes the value as counters wrap. + sb_event_counter_t numNew = numSent - *numRecv; + if (0 == numNew) { + // Queue is empty + return false; + } + + // One element in the ring buffer is always considered dirty. Its the next + // element we will write. It's not safe to read it until numSent has been + // incremented. Thus there are really only (SB_QUEUE_BASE_SW_RAWETHERNETMESSAGE_IMPL_1_SIZE - 1) + // elements in the queue. + *numDropped = (numNew <= SB_QUEUE_BASE_SW_RAWETHERNETMESSAGE_IMPL_1_SIZE - 1) ? 0 : numNew - SB_QUEUE_BASE_SW_RAWETHERNETMESSAGE_IMPL_1_SIZE + 1; + + // Increment numRecv by *numDropped plus one for the element we are about to read. + *numRecv += *numDropped + 1; + + // UNUSED - number of elements left to be consumed + //sb_event_counter_t numRemaining = numSent - *numRecv; + + size_t index = (*numRecv - 1) % SB_QUEUE_BASE_SW_RAWETHERNETMESSAGE_IMPL_1_SIZE; + *data = queue->elt[index]; // Copy data + + // Acquire memory fence - ensure read of data BEFORE reading queue->numSent again + __atomic_thread_fence(__ATOMIC_ACQUIRE); + + if (queue->numSent - *numRecv + 1 < SB_QUEUE_BASE_SW_RAWETHERNETMESSAGE_IMPL_1_SIZE) { + // Sender did not write element we were reading. Copied data is coherent. + return true; + } else { + // Sender may have written element we were reading. Copied data may be incoherent. + // We dropped the element we were trying to read, so increment *numDropped. + ++(*numDropped); + return false; + } +} + +bool sb_queue_base_SW_RawEthernetMessage_Impl_1_is_empty(sb_queue_base_SW_RawEthernetMessage_Impl_1_Recv_t *recvQueue) { + return (recvQueue->queue->numSent == recvQueue->numRecv); +} \ No newline at end of file diff --git a/open-platform-models/isolate-ethernet-simple/microkit/src/sb_queue_base_SW_SizedEthernetMessage_Impl_1.c b/open-platform-models/isolate-ethernet-simple/microkit/src/sb_queue_base_SW_SizedEthernetMessage_Impl_1.c new file mode 100644 index 0000000..904c39b --- /dev/null +++ b/open-platform-models/isolate-ethernet-simple/microkit/src/sb_queue_base_SW_SizedEthernetMessage_Impl_1.c @@ -0,0 +1,117 @@ +/* + * Copyright 2017, Data61 + * Commonwealth Scientific and Industrial Research Organisation (CSIRO) + * ABN 41 687 119 230. + * + * Copyright 2019 Adventium Labs + * Modifications made to original + * + * This software may be distributed and modified according to the terms of + * the BSD 2-Clause license. Note that NO WARRANTY is provided. + * See "LICENSE_BSD2.txt" for details. + * + * @TAG(DATA61_Adventium_BSD) + */ + +#include +#include +#include + +//------------------------------------------------------------------------------ +// Sender API +// +// See sb_queue_base_SW_SizedEthernetMessage_Impl_1.h for API documentation. Only implementation details are documented here. + +void sb_queue_base_SW_SizedEthernetMessage_Impl_1_init(sb_queue_base_SW_SizedEthernetMessage_Impl_1_t *queue) { + // NOOP for now. C's struct initialization is sufficient. If we ever do need + // initialization logic, we may also need to synchronize with receiver + // startup. +} + +void sb_queue_base_SW_SizedEthernetMessage_Impl_1_enqueue( + sb_queue_base_SW_SizedEthernetMessage_Impl_1_t *queue, + base_SW_SizedEthernetMessage_Impl *data) { + + // Simple ring with one dirty element that will be written next. Only one + // writer, so no need for any synchronization. + // elt[queue->numSent % SB_QUEUE_BASE_SW_SIZEDETHERNETMESSAGE_IMPL_1_SIZE] + // is always considered dirty. So do not advance queue->NumSent + // till AFTER data is copied. + + size_t index = queue->numSent % SB_QUEUE_BASE_SW_SIZEDETHERNETMESSAGE_IMPL_1_SIZE; + + queue->elt[index] = *data; // Copy data into queue + + // Release memory fence - ensure that data write above completes BEFORE we advance queue->numSent + __atomic_thread_fence(__ATOMIC_RELEASE); + + ++(queue->numSent); +} + +//------------------------------------------------------------------------------ +// Receiver API +// +// See sb_queue_base_SW_SizedEthernetMessage_Impl_1.h for API documentation. Only implementation details are documented here. + +void sb_queue_base_SW_SizedEthernetMessage_Impl_1_Recv_init( + sb_queue_base_SW_SizedEthernetMessage_Impl_1_Recv_t *recvQueue, + sb_queue_base_SW_SizedEthernetMessage_Impl_1_t *queue) { + + recvQueue->numRecv = 0; + recvQueue->queue = queue; +} + +bool sb_queue_base_SW_SizedEthernetMessage_Impl_1_dequeue( + sb_queue_base_SW_SizedEthernetMessage_Impl_1_Recv_t *recvQueue, + sb_event_counter_t *numDropped, + base_SW_SizedEthernetMessage_Impl *data) { + + sb_event_counter_t *numRecv = &recvQueue->numRecv; + sb_queue_base_SW_SizedEthernetMessage_Impl_1_t *queue = recvQueue->queue; + + // Get a copy of numSent so we can see if it changes during read + sb_event_counter_t numSent = queue->numSent; + + // Acquire memory fence - ensure read of queue->numSent BEFORE reading data + __atomic_thread_fence(__ATOMIC_ACQUIRE); + + // How many new elements have been sent? Since we are using unsigned + // integers, this correctly computes the value as counters wrap. + sb_event_counter_t numNew = numSent - *numRecv; + if (0 == numNew) { + // Queue is empty + return false; + } + + // One element in the ring buffer is always considered dirty. Its the next + // element we will write. It's not safe to read it until numSent has been + // incremented. Thus there are really only (SB_QUEUE_BASE_SW_SIZEDETHERNETMESSAGE_IMPL_1_SIZE - 1) + // elements in the queue. + *numDropped = (numNew <= SB_QUEUE_BASE_SW_SIZEDETHERNETMESSAGE_IMPL_1_SIZE - 1) ? 0 : numNew - SB_QUEUE_BASE_SW_SIZEDETHERNETMESSAGE_IMPL_1_SIZE + 1; + + // Increment numRecv by *numDropped plus one for the element we are about to read. + *numRecv += *numDropped + 1; + + // UNUSED - number of elements left to be consumed + //sb_event_counter_t numRemaining = numSent - *numRecv; + + size_t index = (*numRecv - 1) % SB_QUEUE_BASE_SW_SIZEDETHERNETMESSAGE_IMPL_1_SIZE; + *data = queue->elt[index]; // Copy data + + // Acquire memory fence - ensure read of data BEFORE reading queue->numSent again + __atomic_thread_fence(__ATOMIC_ACQUIRE); + + if (queue->numSent - *numRecv + 1 < SB_QUEUE_BASE_SW_SIZEDETHERNETMESSAGE_IMPL_1_SIZE) { + // Sender did not write element we were reading. Copied data is coherent. + return true; + } else { + // Sender may have written element we were reading. Copied data may be incoherent. + // We dropped the element we were trying to read, so increment *numDropped. + ++(*numDropped); + return false; + } +} + +bool sb_queue_base_SW_SizedEthernetMessage_Impl_1_is_empty(sb_queue_base_SW_SizedEthernetMessage_Impl_1_Recv_t *recvQueue) { + return (recvQueue->queue->numSent == recvQueue->numRecv); +} \ No newline at end of file diff --git a/open-platform-models/isolate-ethernet-simple/microkit/system.mk b/open-platform-models/isolate-ethernet-simple/microkit/system.mk index 5e3243d..2520c9b 100644 --- a/open-platform-models/isolate-ethernet-simple/microkit/system.mk +++ b/open-platform-models/isolate-ethernet-simple/microkit/system.mk @@ -36,14 +36,7 @@ LDFLAGS := -L$(BOARD_DIR)/lib LIBS := --start-group -lmicrokit -Tmicrokit.ld --end-group -PRINTF_OBJS := printf.o util.o -SEL4_ARDUPILOT_ARDUPILOT_MON_OBJS := $(PRINTF_OBJS) seL4_ArduPilot_ArduPilot_MON.o -SEL4_ARDUPILOT_ARDUPILOT_OBJS := $(PRINTF_OBJS) seL4_ArduPilot_ArduPilot.o -SEL4_FIREWALL_FIREWALL_MON_OBJS := $(PRINTF_OBJS) seL4_Firewall_Firewall_MON.o -SEL4_FIREWALL_FIREWALL_OBJS := $(PRINTF_OBJS) seL4_Firewall_Firewall.o -SEL4_LOWLEVELETHERNETDRIVER_LOWLEVELETHERNETDRIVER_MON_OBJS := $(PRINTF_OBJS) seL4_LowLevelEthernetDriver_LowLevelEthernetDriver_MON.o -SEL4_LOWLEVELETHERNETDRIVER_LOWLEVELETHERNETDRIVER_OBJS := $(PRINTF_OBJS) seL4_LowLevelEthernetDriver_LowLevelEthernetDriver.o -PACER_OBJS := $(PRINTF_OBJS) pacer.o +TYPE_OBJS := printf.o util.o sb_queue_base_SW_RawEthernetMessage_Impl_1.o sb_queue_base_SW_RawEthernetMessage_Impl_1.o sb_queue_base_SW_SizedEthernetMessage_Impl_1.o sb_queue_base_SW_RawEthernetMessage_Impl_1.o SYSTEM_FILE := ${TOP}/microkit.system @@ -68,6 +61,22 @@ printf.o: ${TOP}/src/printf.c Makefile util.o: ${TOP}/src/util.c Makefile $(CC) -c $(CFLAGS) $< -o $@ -I${TOP}/include +sb_queue_base_SW_RawEthernetMessage_Impl_1.o: ${TOP}/src/sb_queue_base_SW_RawEthernetMessage_Impl_1.c Makefile + $(CC) -c $(CFLAGS) $< -o $@ -I${TOP}/include + + +sb_queue_base_SW_RawEthernetMessage_Impl_1.o: ${TOP}/src/sb_queue_base_SW_RawEthernetMessage_Impl_1.c Makefile + $(CC) -c $(CFLAGS) $< -o $@ -I${TOP}/include + + +sb_queue_base_SW_SizedEthernetMessage_Impl_1.o: ${TOP}/src/sb_queue_base_SW_SizedEthernetMessage_Impl_1.c Makefile + $(CC) -c $(CFLAGS) $< -o $@ -I${TOP}/include + + +sb_queue_base_SW_RawEthernetMessage_Impl_1.o: ${TOP}/src/sb_queue_base_SW_RawEthernetMessage_Impl_1.c Makefile + $(CC) -c $(CFLAGS) $< -o $@ -I${TOP}/include + + # monitor seL4_ArduPilot_ArduPilot_MON.o: ${TOP}/components/seL4_ArduPilot_ArduPilot/src/seL4_ArduPilot_ArduPilot_MON.c Makefile $(CC) -c $(CFLAGS) $< -o $@ -I${TOP}/include -I${TOP}/components/seL4_ArduPilot_ArduPilot/include @@ -104,25 +113,25 @@ seL4_LowLevelEthernetDriver_LowLevelEthernetDriver.o: ${TOP}/components/seL4_Low pacer.o: ${TOP}/components/pacer/src/pacer.c Makefile $(CC) -c $(CFLAGS) $< -o $@ -I${TOP}/include -seL4_ArduPilot_ArduPilot_MON.elf: $(PRINTF_OBJS) seL4_ArduPilot_ArduPilot_MON.o +seL4_ArduPilot_ArduPilot_MON.elf: $(TYPE_OBJS) seL4_ArduPilot_ArduPilot_MON.o $(LD) $(LDFLAGS) $^ $(LIBS) -o $@ -seL4_ArduPilot_ArduPilot.elf: $(PRINTF_OBJS) seL4_ArduPilot_ArduPilot_user.o seL4_ArduPilot_ArduPilot.o +seL4_ArduPilot_ArduPilot.elf: $(TYPE_OBJS) seL4_ArduPilot_ArduPilot_user.o seL4_ArduPilot_ArduPilot.o $(LD) $(LDFLAGS) $^ $(LIBS) -o $@ -seL4_Firewall_Firewall_MON.elf: $(PRINTF_OBJS) seL4_Firewall_Firewall_MON.o +seL4_Firewall_Firewall_MON.elf: $(TYPE_OBJS) seL4_Firewall_Firewall_MON.o $(LD) $(LDFLAGS) $^ $(LIBS) -o $@ -seL4_Firewall_Firewall.elf: $(PRINTF_OBJS) seL4_Firewall_Firewall_user.o seL4_Firewall_Firewall.o +seL4_Firewall_Firewall.elf: $(TYPE_OBJS) seL4_Firewall_Firewall_user.o seL4_Firewall_Firewall.o $(LD) $(LDFLAGS) $^ $(LIBS) -o $@ -seL4_LowLevelEthernetDriver_LowLevelEthernetDriver_MON.elf: $(PRINTF_OBJS) seL4_LowLevelEthernetDriver_LowLevelEthernetDriver_MON.o +seL4_LowLevelEthernetDriver_LowLevelEthernetDriver_MON.elf: $(TYPE_OBJS) seL4_LowLevelEthernetDriver_LowLevelEthernetDriver_MON.o $(LD) $(LDFLAGS) $^ $(LIBS) -o $@ -seL4_LowLevelEthernetDriver_LowLevelEthernetDriver.elf: $(PRINTF_OBJS) seL4_LowLevelEthernetDriver_LowLevelEthernetDriver_user.o seL4_LowLevelEthernetDriver_LowLevelEthernetDriver.o +seL4_LowLevelEthernetDriver_LowLevelEthernetDriver.elf: $(TYPE_OBJS) seL4_LowLevelEthernetDriver_LowLevelEthernetDriver_user.o seL4_LowLevelEthernetDriver_LowLevelEthernetDriver.o $(LD) $(LDFLAGS) $^ $(LIBS) -o $@ -pacer.elf: $(PRINTF_OBJS) pacer.o +pacer.elf: $(TYPE_OBJS) pacer.o $(LD) $(LDFLAGS) $^ $(LIBS) -o $@ $(IMAGE_FILE): $(IMAGES) $(SYSTEM_FILE)