diff --git a/dep/sddf b/dep/sddf
index 2cae425f..8a06603a 160000
--- a/dep/sddf
+++ b/dep/sddf
@@ -1 +1 @@
-Subproject commit 2cae425f735d6dd214bdb285e89275a87625bba3
+Subproject commit 8a06603a35d70a939960f1acaa379acb84ca768a
diff --git a/examples/virtio/board/odroidc4/virtio.system b/examples/virtio/board/odroidc4/virtio.system
index 4f142dcd..f0d98444 100644
--- a/examples/virtio/board/odroidc4/virtio.system
+++ b/examples/virtio/board/odroidc4/virtio.system
@@ -27,7 +27,7 @@
-
+
@@ -50,7 +50,7 @@
-
+
@@ -165,17 +165,17 @@
-
+
-
+
-
+
@@ -207,7 +207,7 @@
-
+
@@ -221,18 +221,18 @@
-
-
-
-
-
-
-
-
+
+
+
+
+
+
+
+
-
+
-
+
diff --git a/examples/virtio/board/qemu_virt_aarch64/virtio.system b/examples/virtio/board/qemu_virt_aarch64/virtio.system
index 545db7c7..92ecb996 100644
--- a/examples/virtio/board/qemu_virt_aarch64/virtio.system
+++ b/examples/virtio/board/qemu_virt_aarch64/virtio.system
@@ -23,7 +23,7 @@
-
+
@@ -47,7 +47,7 @@
-
+
@@ -164,17 +164,17 @@
-
+
-
+
-
+
@@ -200,7 +200,7 @@
-
+
@@ -214,18 +214,18 @@
-
-
-
-
-
-
-
-
+
+
+
+
+
+
+
+
-
+
-
+
diff --git a/examples/virtio/client_vmm.c b/examples/virtio/client_vmm.c
index ea1086a6..1988db76 100644
--- a/examples/virtio/client_vmm.c
+++ b/examples/virtio/client_vmm.c
@@ -41,7 +41,6 @@ extern char _guest_initrd_image_end[];
/* Microkit will set this variable to the start of the guest RAM memory region. */
uintptr_t guest_ram_vaddr;
-
/* Virtio Console */
#define SERIAL_VIRT_TX_CH 1
#define SERIAL_VIRT_RX_CH 2
@@ -67,19 +66,17 @@ static struct virtio_console_device virtio_console;
#define VIRTIO_BLK_BASE (0x150000)
#define VIRTIO_BLK_SIZE (0x1000)
-uintptr_t blk_req_queue;
-uintptr_t blk_resp_queue;
+blk_req_queue_t *blk_req_queue;
+blk_resp_queue_t *blk_resp_queue;
uintptr_t blk_data;
-uintptr_t blk_config;
+blk_storage_info_t *blk_storage_info;
static struct virtio_blk_device virtio_blk;
void init(void)
{
- blk_storage_info_t *storage_info = (blk_storage_info_t *)blk_config;
-
/* Busy wait until blk device is ready */
- while (!blk_storage_is_ready(storage_info));
+ while (!blk_storage_is_ready(blk_storage_info));
/* Initialise the VMM, the VCPU(s), and start the guest */
LOG_VMM("starting \"%s\"\n", microkit_name);
@@ -111,32 +108,33 @@ void init(void)
/* Initialise our sDDF ring buffers for the serial device */
serial_queue_handle_t serial_rxq, serial_txq;
- serial_cli_queue_init_sys(microkit_name, &serial_rxq, serial_rx_queue, serial_rx_data, &serial_txq, serial_tx_queue, serial_tx_data);
+ serial_cli_queue_init_sys(microkit_name, &serial_rxq, serial_rx_queue, serial_rx_data, &serial_txq, serial_tx_queue,
+ serial_tx_data);
/* Initialise virtIO console device */
success = virtio_mmio_console_init(&virtio_console,
- VIRTIO_CONSOLE_BASE,
- VIRTIO_CONSOLE_SIZE,
- VIRTIO_CONSOLE_IRQ,
- &serial_rxq, &serial_txq,
- SERIAL_VIRT_TX_CH);
+ VIRTIO_CONSOLE_BASE,
+ VIRTIO_CONSOLE_SIZE,
+ VIRTIO_CONSOLE_IRQ,
+ &serial_rxq, &serial_txq,
+ SERIAL_VIRT_TX_CH);
/* virtIO block */
/* Initialise our sDDF queues for the block device */
blk_queue_handle_t blk_queue_h;
blk_queue_init(&blk_queue_h,
- (blk_req_queue_t *)blk_req_queue,
- (blk_resp_queue_t *)blk_resp_queue,
- blk_cli_queue_size(microkit_name));
+ blk_req_queue,
+ blk_resp_queue,
+ blk_cli_queue_capacity(microkit_name));
/* Initialise virtIO block device */
success = virtio_mmio_blk_init(&virtio_blk,
- VIRTIO_BLK_BASE, VIRTIO_BLK_SIZE, VIRTIO_BLK_IRQ,
- blk_data,
- BLK_DATA_SIZE,
- storage_info,
- &blk_queue_h,
- BLK_CH);
+ VIRTIO_BLK_BASE, VIRTIO_BLK_SIZE, VIRTIO_BLK_IRQ,
+ blk_data,
+ BLK_DATA_SIZE,
+ blk_storage_info,
+ &blk_queue_h,
+ BLK_CH);
assert(success);
/* Finally start the guest */
@@ -161,7 +159,8 @@ void notified(microkit_channel ch)
}
}
-seL4_Bool fault(microkit_child child, microkit_msginfo msginfo, microkit_msginfo *reply_msginfo) {
+seL4_Bool fault(microkit_child child, microkit_msginfo msginfo, microkit_msginfo *reply_msginfo)
+{
bool success = fault_handle(child, msginfo);
if (success) {
/* Now that we have handled the fault successfully, we reply to it so
diff --git a/examples/virtio/include/blk_config.h b/examples/virtio/include/blk_config.h
index bd7ec1de..b48d3a0d 100644
--- a/examples/virtio/include/blk_config.h
+++ b/examples/virtio/include/blk_config.h
@@ -15,13 +15,11 @@
#define BLK_NAME_CLI0 "CLIENT_VMM-1"
#define BLK_NAME_CLI1 "CLIENT_VMM-2"
-#define BLK_QUEUE_SIZE_CLI0 1024
-#define BLK_QUEUE_SIZE_CLI1 1024
-#define BLK_QUEUE_SIZE_DRIV (BLK_QUEUE_SIZE_CLI0 + BLK_QUEUE_SIZE_CLI1)
+#define BLK_QUEUE_CAPACITY_CLI0 1024
+#define BLK_QUEUE_CAPACITY_CLI1 1024
+#define BLK_QUEUE_CAPACITY_DRIV (BLK_QUEUE_CAPACITY_CLI0 + BLK_QUEUE_CAPACITY_CLI1)
#define BLK_REGION_SIZE 0x200000
-#define BLK_CONFIG_REGION_SIZE_CLI0 BLK_REGION_SIZE
-#define BLK_CONFIG_REGION_SIZE_CLI1 BLK_REGION_SIZE
#define BLK_DATA_REGION_SIZE_CLI0 BLK_REGION_SIZE
#define BLK_DATA_REGION_SIZE_CLI1 BLK_REGION_SIZE
@@ -40,13 +38,13 @@ _Static_assert(BLK_DATA_REGION_SIZE_DRIV >= BLK_TRANSFER_SIZE &&BLK_DATA_REGION_
static const int blk_partition_mapping[BLK_NUM_CLIENTS] = { 0, 1 };
-static inline blk_storage_info_t *blk_virt_cli_config_info(blk_storage_info_t *info, unsigned int id)
+static inline blk_storage_info_t *blk_virt_cli_storage_info(blk_storage_info_t *info, unsigned int id)
{
switch (id) {
case 0:
return info;
case 1:
- return (blk_storage_info_t *)((uintptr_t)info + BLK_CONFIG_REGION_SIZE_CLI0);
+ return (blk_storage_info_t *)((uintptr_t)info + BLK_STORAGE_INFO_REGION_SIZE);
default:
return NULL;
}
@@ -100,24 +98,24 @@ static inline blk_resp_queue_t *blk_virt_cli_resp_queue(blk_resp_queue_t *resp,
}
}
-static inline uint32_t blk_virt_cli_queue_size(unsigned int id)
+static inline uint32_t blk_virt_cli_queue_capacity(unsigned int id)
{
switch (id) {
case 0:
- return BLK_QUEUE_SIZE_CLI0;
+ return BLK_QUEUE_CAPACITY_CLI0;
case 1:
- return BLK_QUEUE_SIZE_CLI1;
+ return BLK_QUEUE_CAPACITY_CLI1;
default:
return 0;
}
}
-static inline uint32_t blk_cli_queue_size(char *pd_name)
+static inline uint32_t blk_cli_queue_capacity(char *pd_name)
{
if (!sddf_strcmp(pd_name, BLK_NAME_CLI0)) {
- return BLK_QUEUE_SIZE_CLI0;
+ return BLK_QUEUE_CAPACITY_CLI0;
} else if (!sddf_strcmp(pd_name, BLK_NAME_CLI1)) {
- return BLK_QUEUE_SIZE_CLI1;
+ return BLK_QUEUE_CAPACITY_CLI1;
} else {
return 0;
}
diff --git a/examples/virtio/include/serial_config.h b/examples/virtio/include/serial_config.h
index 6850e054..691eaaf7 100644
--- a/examples/virtio/include/serial_config.h
+++ b/examples/virtio/include/serial_config.h
@@ -40,23 +40,23 @@
#define SERIAL_VIRT_TX_NAME "serial_virt_tx"
#define SERIAL_DRIVER_NAME "uart_driver"
-#define SERIAL_QUEUE_SIZE 0x1000
-#define SERIAL_DATA_REGION_SIZE 0x2000
-
-#define SERIAL_TX_DATA_REGION_SIZE_DRIV SERIAL_DATA_REGION_SIZE
-#define SERIAL_TX_DATA_REGION_SIZE_CLI0 SERIAL_DATA_REGION_SIZE
-#define SERIAL_TX_DATA_REGION_SIZE_CLI1 SERIAL_DATA_REGION_SIZE
-#define SERIAL_TX_DATA_REGION_SIZE_CLI2 SERIAL_DATA_REGION_SIZE
-
-#define SERIAL_RX_DATA_REGION_SIZE_DRIV SERIAL_DATA_REGION_SIZE
-#define SERIAL_RX_DATA_REGION_SIZE_CLI0 SERIAL_DATA_REGION_SIZE
-#define SERIAL_RX_DATA_REGION_SIZE_CLI1 SERIAL_DATA_REGION_SIZE
-#define SERIAL_RX_DATA_REGION_SIZE_CLI2 SERIAL_DATA_REGION_SIZE
-
-#define SERIAL_MAX_TX_DATA_SIZE MAX(SERIAL_TX_DATA_REGION_SIZE_DRIV, MAX(SERIAL_TX_DATA_REGION_SIZE_CLI2, MAX(SERIAL_TX_DATA_REGION_SIZE_CLI0, SERIAL_TX_DATA_REGION_SIZE_CLI1)))
-#define SERIAL_MAX_RX_DATA_SIZE MAX(SERIAL_RX_DATA_REGION_SIZE_DRIV, MAX(SERIAL_RX_DATA_REGION_SIZE_CLI2, MAX(SERIAL_RX_DATA_REGION_SIZE_CLI0, SERIAL_RX_DATA_REGION_SIZE_CLI1)))
-#define SERIAL_MAX_DATA_SIZE MAX(SERIAL_MAX_TX_DATA_SIZE, SERIAL_MAX_RX_DATA_SIZE)
-_Static_assert(SERIAL_MAX_DATA_SIZE < UINT32_MAX,
+#define SERIAL_QUEUE_CAPACITY 0x1000
+#define SERIAL_DATA_REGION_CAPACITY 0x2000
+
+#define SERIAL_TX_DATA_REGION_CAPACITY_DRIV SERIAL_DATA_REGION_CAPACITY
+#define SERIAL_TX_DATA_REGION_CAPACITY_CLI0 SERIAL_DATA_REGION_CAPACITY
+#define SERIAL_TX_DATA_REGION_CAPACITY_CLI1 SERIAL_DATA_REGION_CAPACITY
+#define SERIAL_TX_DATA_REGION_CAPACITY_CLI2 SERIAL_DATA_REGION_CAPACITY
+
+#define SERIAL_RX_DATA_REGION_CAPACITY_DRIV SERIAL_DATA_REGION_CAPACITY
+#define SERIAL_RX_DATA_REGION_CAPACITY_CLI0 SERIAL_DATA_REGION_CAPACITY
+#define SERIAL_RX_DATA_REGION_CAPACITY_CLI1 SERIAL_DATA_REGION_CAPACITY
+#define SERIAL_RX_DATA_REGION_CAPACITY_CLI2 SERIAL_DATA_REGION_CAPACITY
+
+#define SERIAL_MAX_TX_DATA_CAPACITY MAX(SERIAL_TX_DATA_REGION_CAPACITY_DRIV, MAX(SERIAL_TX_DATA_REGION_CAPACITY_CLI2, MAX(SERIAL_TX_DATA_REGION_CAPACITY_CLI0, SERIAL_TX_DATA_REGION_CAPACITY_CLI1)))
+#define SERIAL_MAX_RX_DATA_CAPACITY MAX(SERIAL_RX_DATA_REGION_CAPACITY_DRIV, MAX(SERIAL_RX_DATA_REGION_CAPACITY_CLI2, MAX(SERIAL_RX_DATA_REGION_CAPACITY_CLI0, SERIAL_RX_DATA_REGION_CAPACITY_CLI1)))
+#define SERIAL_MAX_DATA_CAPACITY MAX(SERIAL_MAX_TX_DATA_CAPACITY, SERIAL_MAX_RX_DATA_CAPACITY)
+_Static_assert(SERIAL_MAX_DATA_CAPACITY < UINT32_MAX,
"Data regions must be smaller than UINT32 max to correctly use queue data structure.");
static inline void serial_cli_queue_init_sys(char *pd_name, serial_queue_handle_t *rx_queue_handle,
@@ -64,14 +64,14 @@ static inline void serial_cli_queue_init_sys(char *pd_name, serial_queue_handle_
serial_queue_t *tx_queue, char *tx_data)
{
if (!sddf_strcmp(pd_name, SERIAL_CLI0_NAME)) {
- serial_queue_init(rx_queue_handle, rx_queue, SERIAL_RX_DATA_REGION_SIZE_CLI0, rx_data);
- serial_queue_init(tx_queue_handle, tx_queue, SERIAL_TX_DATA_REGION_SIZE_CLI0, tx_data);
+ serial_queue_init(rx_queue_handle, rx_queue, SERIAL_RX_DATA_REGION_CAPACITY_CLI0, rx_data);
+ serial_queue_init(tx_queue_handle, tx_queue, SERIAL_TX_DATA_REGION_CAPACITY_CLI0, tx_data);
} else if (!sddf_strcmp(pd_name, SERIAL_CLI1_NAME)) {
- serial_queue_init(rx_queue_handle, rx_queue, SERIAL_RX_DATA_REGION_SIZE_CLI1, rx_data);
- serial_queue_init(tx_queue_handle, tx_queue, SERIAL_TX_DATA_REGION_SIZE_CLI1, tx_data);
+ serial_queue_init(rx_queue_handle, rx_queue, SERIAL_RX_DATA_REGION_CAPACITY_CLI1, rx_data);
+ serial_queue_init(tx_queue_handle, tx_queue, SERIAL_TX_DATA_REGION_CAPACITY_CLI1, tx_data);
} else if (!sddf_strcmp(pd_name, SERIAL_CLI2_NAME)) {
- serial_queue_init(rx_queue_handle, rx_queue, SERIAL_RX_DATA_REGION_SIZE_CLI2, rx_data);
- serial_queue_init(tx_queue_handle, tx_queue, SERIAL_TX_DATA_REGION_SIZE_CLI2, tx_data);
+ serial_queue_init(rx_queue_handle, rx_queue, SERIAL_RX_DATA_REGION_CAPACITY_CLI2, rx_data);
+ serial_queue_init(tx_queue_handle, tx_queue, SERIAL_TX_DATA_REGION_CAPACITY_CLI2, tx_data);
}
}
@@ -80,19 +80,19 @@ static inline void serial_virt_queue_init_sys(char *pd_name, serial_queue_handle
{
uintptr_t cli_queue_ptr = (uintptr_t)cli_queue;
if (!sddf_strcmp(pd_name, SERIAL_VIRT_RX_NAME)) {
- serial_queue_init(cli_queue_handle, cli_queue, SERIAL_RX_DATA_REGION_SIZE_CLI0, cli_data);
- serial_queue_init(&cli_queue_handle[1], (serial_queue_t *)(cli_queue_ptr + SERIAL_QUEUE_SIZE),
- SERIAL_RX_DATA_REGION_SIZE_CLI1, (char *)(cli_data + SERIAL_RX_DATA_REGION_SIZE_CLI0));
- serial_queue_init(&cli_queue_handle[2], (serial_queue_t *)(cli_queue_ptr + 2 * SERIAL_QUEUE_SIZE),
- SERIAL_RX_DATA_REGION_SIZE_CLI2,
- (char *)(cli_data + SERIAL_RX_DATA_REGION_SIZE_CLI0 + SERIAL_RX_DATA_REGION_SIZE_CLI1));
+ serial_queue_init(cli_queue_handle, cli_queue, SERIAL_RX_DATA_REGION_CAPACITY_CLI0, cli_data);
+ serial_queue_init(&cli_queue_handle[1], (serial_queue_t *)(cli_queue_ptr + SERIAL_QUEUE_CAPACITY),
+ SERIAL_RX_DATA_REGION_CAPACITY_CLI1, (char *)(cli_data + SERIAL_RX_DATA_REGION_CAPACITY_CLI0));
+ serial_queue_init(&cli_queue_handle[2], (serial_queue_t *)(cli_queue_ptr + 2 * SERIAL_QUEUE_CAPACITY),
+ SERIAL_RX_DATA_REGION_CAPACITY_CLI2,
+ (char *)(cli_data + SERIAL_RX_DATA_REGION_CAPACITY_CLI0 + SERIAL_RX_DATA_REGION_CAPACITY_CLI1));
} else if (!sddf_strcmp(pd_name, SERIAL_VIRT_TX_NAME)) {
- serial_queue_init(cli_queue_handle, cli_queue, SERIAL_TX_DATA_REGION_SIZE_CLI0, cli_data);
- serial_queue_init(&cli_queue_handle[1], (serial_queue_t *)(cli_queue_ptr + SERIAL_QUEUE_SIZE),
- SERIAL_TX_DATA_REGION_SIZE_CLI1, cli_data + SERIAL_TX_DATA_REGION_SIZE_CLI0);
- serial_queue_init(&cli_queue_handle[2], (serial_queue_t *)(cli_queue_ptr + 2 * SERIAL_QUEUE_SIZE),
- SERIAL_TX_DATA_REGION_SIZE_CLI2,
- (char *)(cli_data + SERIAL_TX_DATA_REGION_SIZE_CLI0 + SERIAL_TX_DATA_REGION_SIZE_CLI1));
+ serial_queue_init(cli_queue_handle, cli_queue, SERIAL_TX_DATA_REGION_CAPACITY_CLI0, cli_data);
+ serial_queue_init(&cli_queue_handle[1], (serial_queue_t *)(cli_queue_ptr + SERIAL_QUEUE_CAPACITY),
+ SERIAL_TX_DATA_REGION_CAPACITY_CLI1, cli_data + SERIAL_TX_DATA_REGION_CAPACITY_CLI0);
+ serial_queue_init(&cli_queue_handle[2], (serial_queue_t *)(cli_queue_ptr + 2 * SERIAL_QUEUE_CAPACITY),
+ SERIAL_TX_DATA_REGION_CAPACITY_CLI2,
+ (char *)(cli_data + SERIAL_TX_DATA_REGION_CAPACITY_CLI0 + SERIAL_TX_DATA_REGION_CAPACITY_CLI1));
}
}
diff --git a/src/virtio/console.c b/src/virtio/console.c
index c21311a9..35f585d4 100644
--- a/src/virtio/console.c
+++ b/src/virtio/console.c
@@ -140,7 +140,7 @@ static bool virtio_console_handle_tx(struct virtio_device *dev)
transferred = true;
}
- memcpy(console->txq.data_region + (console->txq.queue->tail % console->txq.size),
+ memcpy(console->txq.data_region + (console->txq.queue->tail % console->txq.capacity),
(char *)(desc.addr + (desc.len - bytes_remain)), to_transfer);
serial_update_visible_tail(&console->txq, console->txq.queue->tail + to_transfer);
diff --git a/tools/linux/uio_drivers/blk/blk.c b/tools/linux/uio_drivers/blk/blk.c
index b1090c00..fc224f82 100644
--- a/tools/linux/uio_drivers/blk/blk.c
+++ b/tools/linux/uio_drivers/blk/blk.c
@@ -64,7 +64,7 @@ int driver_init(void **maps, uintptr_t *maps_phys, int num_maps, int argc, char
LOG_UIO_BLOCK("maps_phys[0]: 0x%lx, maps_phys[1]: 0x%lx, maps_phys[2]: 0x%lx, maps_phys[3]: 0x%lx\n", maps_phys[0],
maps_phys[1], maps_phys[2], maps_phys[3]);
- blk_queue_init(&h, req_queue, resp_queue, BLK_QUEUE_SIZE_DRIV);
+ blk_queue_init(&h, req_queue, resp_queue, BLK_QUEUE_CAPACITY_DRIV);
storage_fd = open(storage_path, O_RDWR);
if (storage_fd < 0) {