Update to latest HAMR which uses queuing

open-platform-models/isolate-ethernet-simple/microkit/components/seL4_ArduPilot_ArduPilot/include/seL4_ArduPilot_ArduPilot.h

@@ -1,7 +1,7 @@
 #include <printf.h>
 #include <stdint.h>
 #include <microkit.h>
-#include <types.h>
+#include <sb_types.h>
 
-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);

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();
 }
 

open-platform-models/isolate-ethernet-simple/microkit/components/seL4_Firewall_Firewall/include/seL4_Firewall_Firewall.h

@@ -1,9 +1,9 @@
 #include <printf.h>
 #include <stdint.h>
 #include <microkit.h>
-#include <types.h>
+#include <sb_types.h>
 
-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);

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();
 }
 

open-platform-models/isolate-ethernet-simple/microkit/components/seL4_LowLevelEthernetDriver_LowLevelEthernetDriver/include/seL4_LowLevelEthernetDriver_LowLevelEthernetDriver.h

@@ -1,7 +1,7 @@
 #include <printf.h>
 #include <stdint.h>
 #include <microkit.h>
-#include <types.h>
+#include <sb_types.h>
 
-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);

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();
 }
 

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 <stdint.h>
+
+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

open-platform-models/isolate-ethernet-simple/microkit/include/sb_event_counter.h

@@ -0,0 +1,5 @@
+#pragma once
+
+#include <stdint.h>
+
+typedef _Atomic uintmax_t sb_event_counter_t;

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 <sb_event_counter.h>
+#include <sb_aadl_types.h>
+#include <stdbool.h>
+
+// 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);