Skip to content

Commit

Permalink
Update serial config files to new format
Browse files Browse the repository at this point in the history 
Signed-off-by: Courtney Darville <[email protected]>
  • Loading branch information
@Courtney3141
Courtney3141 committed Oct 13, 2024
1 parent 6affa35 commit 9fe672d
Show file tree
Hide file tree
Showing 9 changed files with 172 additions and 114 deletions.
22 changes: 9 additions & 13 deletions benchmark/benchmark.c
View file
Original file line number Diff line number Diff line change
Expand Up @@ -93,8 +93,7 @@ static void benchmark_print_IPC_data(uint64_t *buffer, uint32_t id)
number_schedules = buffer[BENCHMARK_TCB_NUMBER_SCHEDULES];
kernel = buffer[BENCHMARK_TCB_KERNEL_UTILISATION];
entries = buffer[BENCHMARK_TCB_NUMBER_KERNEL_ENTRIES];
sddf_printf("Utilisation details for PD: %s (%x)\n",
pd_id_to_name(id), id);
sddf_printf("Utilisation details for PD: %s (%x)\n", pd_id_to_name(id), id);
}
sddf_printf("{\nKernelUtilisation: %lx\nKernelEntries: "
"%lx\nNumberSchedules: %lx\nTotalUtilisation: %lx\n}\n",
Expand Down Expand Up @@ -219,9 +218,9 @@ void notified(microkit_channel ch)

void init(void)
{
serial_cli_queue_init_sys(microkit_name, NULL, NULL, NULL,
&serial_tx_queue_handle, serial_tx_queue,
serial_tx_data);
uint32_t serial_tx_data_capacity;
serial_cli_data_capacity(microkit_name, NULL, &serial_tx_data_capacity);
serial_queue_init(&serial_tx_queue_handle, serial_tx_queue, serial_tx_data_capacity, serial_tx_data);
serial_putchar_init(SERIAL_TX_CH, &serial_tx_queue_handle);

bench_core_config_info(microkit_name, &core_config);
Expand Down Expand Up @@ -263,20 +262,18 @@ seL4_Bool fault(microkit_child id, microkit_msginfo msginfo, microkit_msginfo *r
sddf_printf("BENCH|LOG: Faulting PD %s (%x)\n", pd_id_to_name(id), id);

seL4_UserContext regs;
seL4_TCB_ReadRegisters(BASE_TCB_CAP + id, false, 0,
sizeof(seL4_UserContext) / sizeof(seL4_Word), &regs);
seL4_TCB_ReadRegisters(BASE_TCB_CAP + id, false, 0, sizeof(seL4_UserContext) / sizeof(seL4_Word), &regs);
sddf_printf("Registers: \npc : %lx\nspsr : %lx\nx0 : %lx\nx1 : %lx\n"
"x2 : %lx\nx3 : %lx\nx4 : %lx\nx5 : %lx\nx6 : %lx\nx7 : %lx\n",
regs.pc, regs.spsr, regs.x0, regs.x1, regs.x2, regs.x3,
regs.x4, regs.x5, regs.x6, regs.x7);
regs.pc, regs.spsr, regs.x0, regs.x1, regs.x2, regs.x3, regs.x4, regs.x5, regs.x6, regs.x7);

switch (microkit_msginfo_get_label(msginfo)) {
case seL4_Fault_CapFault: {
uint64_t ip = seL4_GetMR(seL4_CapFault_IP);
uint64_t fault_addr = seL4_GetMR(seL4_CapFault_Addr);
uint64_t in_recv_phase = seL4_GetMR(seL4_CapFault_InRecvPhase);
sddf_printf("CapFault: ip=%lx fault_addr=%lx in_recv_phase=%s\n",
ip, fault_addr, (in_recv_phase == 0 ? "false" : "true"));
sddf_printf("CapFault: ip=%lx fault_addr=%lx in_recv_phase=%s\n", ip, fault_addr,
(in_recv_phase == 0 ? "false" : "true"));
break;
}
case seL4_Fault_UserException: {
Expand All @@ -288,8 +285,7 @@ seL4_Bool fault(microkit_child id, microkit_msginfo msginfo, microkit_msginfo *r
uint64_t fault_addr = seL4_GetMR(seL4_VMFault_Addr);
uint64_t is_instruction = seL4_GetMR(seL4_VMFault_PrefetchFault);
uint64_t fsr = seL4_GetMR(seL4_VMFault_FSR);
sddf_printf("VMFault: ip=%lx fault_addr=%lx fsr=%lx %s\n",
ip, fault_addr, fsr,
sddf_printf("VMFault: ip=%lx fault_addr=%lx fsr=%lx %s\n", ip, fault_addr, fsr,
(is_instruction ? "(instruction fault)" : "(data fault)"));
break;
}
Expand Down
54 changes: 35 additions & 19 deletions examples/echo_server/include/serial_config/serial_config.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,7 @@
#include <stdint.h>

/* Number of clients that can be connected to the serial server. */
#define SERIAL_NUM_CLIENTS 3
#define NUM_SERIAL_CLIENTS 3

/* Only support transmission and not receive. */
#define SERIAL_TX_ONLY 1
Expand Down Expand Up @@ -41,47 +41,63 @@
#define SERIAL_TX_DATA_REGION_CAPACITY_CLI1 SERIAL_DATA_REGION_CAPACITY
#define SERIAL_TX_DATA_REGION_CAPACITY_CLI2 SERIAL_DATA_REGION_CAPACITY

/* To avoid deadlocks caused when the virtualiser adds colour codes to the
start and end of strings, driver data region must be larger than any
client data region. */
#define SERIAL_MAX_CLIENT_TX_DATA_CAPACITY MAX(SERIAL_TX_DATA_REGION_CAPACITY_CLI2, MAX(SERIAL_TX_DATA_REGION_CAPACITY_CLI0, SERIAL_TX_DATA_REGION_CAPACITY_CLI1))
#if SERIAL_WITH_COLOUR
_Static_assert(SERIAL_TX_DATA_REGION_CAPACITY_DRIV > SERIAL_MAX_CLIENT_TX_DATA_CAPACITY,
"Driver TX data region must be larger than all client data regions in SERIAL_WITH_COLOUR mode.");
#endif

/* Ensure the entire data region can be assigned a unique index by a 32 bit
unsigned. */
#define SERIAL_MAX_DATA_CAPACITY MAX(SERIAL_TX_DATA_REGION_CAPACITY_DRIV, SERIAL_MAX_CLIENT_TX_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,
serial_queue_t *rx_queue,
char *rx_data, serial_queue_handle_t *tx_queue_handle, serial_queue_t *tx_queue, char *tx_data)
static inline void serial_cli_data_capacity(char *pd_name, uint32_t *rx_data_capacity, uint32_t *tx_data_capacity)
{
if (!sddf_strcmp(pd_name, SERIAL_CLI0_NAME)) {
serial_queue_init(tx_queue_handle, tx_queue, SERIAL_TX_DATA_REGION_CAPACITY_CLI0, tx_data);
*tx_data_capacity = SERIAL_TX_DATA_REGION_CAPACITY_CLI0;
} else if (!sddf_strcmp(pd_name, SERIAL_CLI1_NAME)) {
serial_queue_init(tx_queue_handle, tx_queue, SERIAL_TX_DATA_REGION_CAPACITY_CLI1, tx_data);
*tx_data_capacity = SERIAL_TX_DATA_REGION_CAPACITY_CLI1;
} else if (!sddf_strcmp(pd_name, SERIAL_CLI2_NAME)) {
serial_queue_init(tx_queue_handle, tx_queue, SERIAL_TX_DATA_REGION_CAPACITY_CLI2, tx_data);
*tx_data_capacity = SERIAL_TX_DATA_REGION_CAPACITY_CLI2;
}
}

static inline void serial_virt_queue_init_sys(char *pd_name, serial_queue_handle_t *cli_queue_handle,
serial_queue_t *cli_queue, char *cli_data)
typedef struct serial_queue_info {
serial_queue_t *cli_queue;
char *cli_data;
uint32_t capacity;
} serial_queue_info_t;

static inline void serial_virt_queue_info(char *pd_name, serial_queue_t *cli_queue, char *cli_data,
serial_queue_info_t ret[NUM_SERIAL_CLIENTS])
{
if (!sddf_strcmp(pd_name, SERIAL_VIRT_TX_NAME)) {
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 *)((uintptr_t)cli_queue + SERIAL_QUEUE_SIZE),
SERIAL_TX_DATA_REGION_CAPACITY_CLI1, cli_data + SERIAL_TX_DATA_REGION_CAPACITY_CLI0);
serial_queue_init(&cli_queue_handle[2], (serial_queue_t *)((uintptr_t)cli_queue + 2 * SERIAL_QUEUE_SIZE),
SERIAL_TX_DATA_REGION_CAPACITY_CLI2,
cli_data + SERIAL_TX_DATA_REGION_CAPACITY_CLI0 + SERIAL_TX_DATA_REGION_CAPACITY_CLI1);
ret[0] = (serial_queue_info_t) { .cli_queue = cli_queue,
.cli_data = cli_data,
.capacity = SERIAL_TX_DATA_REGION_CAPACITY_CLI0 };
ret[1] =
(serial_queue_info_t) { .cli_queue = (serial_queue_t *)((uintptr_t)ret[0].cli_queue + SERIAL_QUEUE_SIZE),
.cli_data = ret[0].cli_data + ret[0].capacity,
.capacity = SERIAL_TX_DATA_REGION_CAPACITY_CLI1 };
ret[2] =
(serial_queue_info_t) { .cli_queue = (serial_queue_t *)((uintptr_t)ret[1].cli_queue + SERIAL_QUEUE_SIZE),
.cli_data = ret[1].cli_data + ret[1].capacity,
.capacity = SERIAL_TX_DATA_REGION_CAPACITY_CLI2 };
}
}

#if SERIAL_WITH_COLOUR
static inline void serial_channel_names_init(char **client_names)
static inline void serial_channel_names_init(char *pd_name, char *client_names[NUM_SERIAL_CLIENTS])
{
client_names[0] = SERIAL_CLI0_NAME;
client_names[1] = SERIAL_CLI1_NAME;
client_names[2] = SERIAL_CLI2_NAME;
if (!sddf_strcmp(pd_name, SERIAL_VIRT_TX_NAME)) {
client_names[0] = SERIAL_CLI0_NAME;
client_names[1] = SERIAL_CLI1_NAME;
client_names[2] = SERIAL_CLI2_NAME;
}
}
#endif
87 changes: 48 additions & 39 deletions examples/echo_server/include/serial_config_smp/serial_config.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,7 @@
#include <stdint.h>

/* Number of clients that can be connected to the serial server. */
#define SERIAL_NUM_CLIENTS 6
#define NUM_SERIAL_CLIENTS 6

/* Only support transmission and not receive. */
#define SERIAL_TX_ONLY 1
Expand Down Expand Up @@ -62,60 +62,69 @@ _Static_assert(SERIAL_TX_DATA_REGION_CAPACITY_DRIV > SERIAL_MAX_CLIENT_TX_DATA_C
_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,
serial_queue_t *rx_queue, char *rx_data,
serial_queue_handle_t *tx_queue_handle, serial_queue_t *tx_queue,
char *tx_data)
static inline void serial_cli_data_capacity(char *pd_name, uint32_t *rx_data_capacity, uint32_t *tx_data_capacity)
{
if (!sddf_strcmp(pd_name, SERIAL_CLI0_NAME)) {
serial_queue_init(tx_queue_handle, tx_queue, SERIAL_TX_DATA_REGION_CAPACITY_CLI0, tx_data);
*tx_data_capacity = SERIAL_TX_DATA_REGION_CAPACITY_CLI0;
} else if (!sddf_strcmp(pd_name, SERIAL_CLI1_NAME)) {
serial_queue_init(tx_queue_handle, tx_queue, SERIAL_TX_DATA_REGION_CAPACITY_CLI1, tx_data);
*tx_data_capacity = SERIAL_TX_DATA_REGION_CAPACITY_CLI1;
} else if (!sddf_strcmp(pd_name, SERIAL_CLI2_NAME)) {
serial_queue_init(tx_queue_handle, tx_queue, SERIAL_TX_DATA_REGION_CAPACITY_CLI2, tx_data);
*tx_data_capacity = SERIAL_TX_DATA_REGION_CAPACITY_CLI2;
} else if (!sddf_strcmp(pd_name, SERIAL_CLI3_NAME)) {
serial_queue_init(tx_queue_handle, tx_queue, SERIAL_TX_DATA_REGION_CAPACITY_CLI3, tx_data);
*tx_data_capacity = SERIAL_TX_DATA_REGION_CAPACITY_CLI3;
} else if (!sddf_strcmp(pd_name, SERIAL_CLI4_NAME)) {
serial_queue_init(tx_queue_handle, tx_queue, SERIAL_TX_DATA_REGION_CAPACITY_CLI4, tx_data);
*tx_data_capacity = SERIAL_TX_DATA_REGION_CAPACITY_CLI4;
} else if (!sddf_strcmp(pd_name, SERIAL_CLI5_NAME)) {
serial_queue_init(tx_queue_handle, tx_queue, SERIAL_TX_DATA_REGION_CAPACITY_CLI5, tx_data);
*tx_data_capacity = SERIAL_TX_DATA_REGION_CAPACITY_CLI5;
}
}

static inline void serial_virt_queue_init_sys(char *pd_name, serial_queue_handle_t *cli_queue_handle,
serial_queue_t *cli_queue, char *cli_data)
typedef struct serial_queue_info {
serial_queue_t *cli_queue;
char *cli_data;
uint32_t capacity;
} serial_queue_info_t;

static inline void serial_virt_queue_info(char *pd_name, serial_queue_t *cli_queue, char *cli_data,
serial_queue_info_t ret[NUM_SERIAL_CLIENTS])
{
if (!sddf_strcmp(pd_name, SERIAL_VIRT_TX_NAME)) {
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 *)((uintptr_t)cli_queue + SERIAL_QUEUE_SIZE),
SERIAL_TX_DATA_REGION_CAPACITY_CLI1, cli_data + SERIAL_TX_DATA_REGION_CAPACITY_CLI0);
serial_queue_init(&cli_queue_handle[2], (serial_queue_t *)((uintptr_t)cli_queue + 2 * SERIAL_QUEUE_SIZE),
SERIAL_TX_DATA_REGION_CAPACITY_CLI2,
cli_data + SERIAL_TX_DATA_REGION_CAPACITY_CLI0 + SERIAL_TX_DATA_REGION_CAPACITY_CLI1);
serial_queue_init(&cli_queue_handle[3], (serial_queue_t *)((uintptr_t)cli_queue + 3 * SERIAL_QUEUE_SIZE),
SERIAL_TX_DATA_REGION_CAPACITY_CLI3,
cli_data + SERIAL_TX_DATA_REGION_CAPACITY_CLI0 + SERIAL_TX_DATA_REGION_CAPACITY_CLI1
+ SERIAL_TX_DATA_REGION_CAPACITY_CLI2);
serial_queue_init(&cli_queue_handle[4], (serial_queue_t *)((uintptr_t)cli_queue + 4 * SERIAL_QUEUE_SIZE),
SERIAL_TX_DATA_REGION_CAPACITY_CLI4,
cli_data + SERIAL_TX_DATA_REGION_CAPACITY_CLI0 + SERIAL_TX_DATA_REGION_CAPACITY_CLI1
+ SERIAL_TX_DATA_REGION_CAPACITY_CLI2 + SERIAL_TX_DATA_REGION_CAPACITY_CLI3);
serial_queue_init(&cli_queue_handle[5], (serial_queue_t *)((uintptr_t)cli_queue + 5 * SERIAL_QUEUE_SIZE),
SERIAL_TX_DATA_REGION_CAPACITY_CLI5,
cli_data + SERIAL_TX_DATA_REGION_CAPACITY_CLI0 + SERIAL_TX_DATA_REGION_CAPACITY_CLI1
+ SERIAL_TX_DATA_REGION_CAPACITY_CLI2 + SERIAL_TX_DATA_REGION_CAPACITY_CLI3
+ SERIAL_TX_DATA_REGION_CAPACITY_CLI4);
ret[0] = (serial_queue_info_t) { .cli_queue = cli_queue,
.cli_data = cli_data,
.capacity = SERIAL_TX_DATA_REGION_CAPACITY_CLI0 };
ret[1] =
(serial_queue_info_t) { .cli_queue = (serial_queue_t *)((uintptr_t)ret[0].cli_queue + SERIAL_QUEUE_SIZE),
.cli_data = ret[0].cli_data + ret[0].capacity,
.capacity = SERIAL_TX_DATA_REGION_CAPACITY_CLI1 };
ret[2] =
(serial_queue_info_t) { .cli_queue = (serial_queue_t *)((uintptr_t)ret[1].cli_queue + SERIAL_QUEUE_SIZE),
.cli_data = ret[1].cli_data + ret[1].capacity,
.capacity = SERIAL_TX_DATA_REGION_CAPACITY_CLI2 };
ret[3] =
(serial_queue_info_t) { .cli_queue = (serial_queue_t *)((uintptr_t)ret[2].cli_queue + SERIAL_QUEUE_SIZE),
.cli_data = ret[2].cli_data + ret[2].capacity,
.capacity = SERIAL_TX_DATA_REGION_CAPACITY_CLI3 };
ret[4] =
(serial_queue_info_t) { .cli_queue = (serial_queue_t *)((uintptr_t)ret[3].cli_queue + SERIAL_QUEUE_SIZE),
.cli_data = ret[3].cli_data + ret[3].capacity,
.capacity = SERIAL_TX_DATA_REGION_CAPACITY_CLI4 };
ret[5] =
(serial_queue_info_t) { .cli_queue = (serial_queue_t *)((uintptr_t)ret[4].cli_queue + SERIAL_QUEUE_SIZE),
.cli_data = ret[4].cli_data + ret[4].capacity,
.capacity = SERIAL_TX_DATA_REGION_CAPACITY_CLI5 };
}
}

#if SERIAL_WITH_COLOUR
static inline void serial_channel_names_init(char **client_names)
static inline void serial_channel_names_init(char *pd_name, char *client_names[NUM_SERIAL_CLIENTS])
{
client_names[0] = SERIAL_CLI0_NAME;
client_names[1] = SERIAL_CLI1_NAME;
client_names[2] = SERIAL_CLI2_NAME;
client_names[3] = SERIAL_CLI3_NAME;
client_names[4] = SERIAL_CLI4_NAME;
client_names[5] = SERIAL_CLI5_NAME;
if (!sddf_strcmp(pd_name, SERIAL_VIRT_TX_NAME)) {
client_names[0] = SERIAL_CLI0_NAME;
client_names[1] = SERIAL_CLI1_NAME;
client_names[2] = SERIAL_CLI2_NAME;
client_names[3] = SERIAL_CLI3_NAME;
client_names[4] = SERIAL_CLI4_NAME;
client_names[5] = SERIAL_CLI5_NAME;
}
}
#endif
12 changes: 7 additions & 5 deletions examples/echo_server/lwip.c
View file
Original file line number Diff line number Diff line change
Expand Up @@ -286,13 +286,15 @@ static void netif_status_callback(struct netif *netif)

void init(void)
{
serial_cli_queue_init_sys(microkit_name, NULL, NULL, NULL, &serial_tx_queue_handle, serial_tx_queue, serial_tx_data);
uint32_t serial_tx_data_capacity;
serial_cli_data_capacity(microkit_name, NULL, &serial_tx_data_capacity);
serial_queue_init(&serial_tx_queue_handle, serial_tx_queue, serial_tx_data_capacity, serial_tx_data);
serial_putchar_init(SERIAL_TX_CH, &serial_tx_queue_handle);

size_t rx_capacity, tx_capacity;
net_cli_queue_capacity(microkit_name, &rx_capacity, &tx_capacity);
net_queue_init(&state.rx_queue, rx_free, rx_active, rx_capacity);
net_queue_init(&state.tx_queue, tx_free, tx_active, tx_capacity);
size_t net_rx_capacity, net_tx_capacity;
net_cli_queue_capacity(microkit_name, &net_rx_capacity, &net_tx_capacity);
net_queue_init(&state.rx_queue, rx_free, rx_active, net_rx_capacity);
net_queue_init(&state.tx_queue, tx_free, tx_active, net_tx_capacity);
net_buffers_init(&state.tx_queue, 0);

lwip_init();
Expand Down
4 changes: 2 additions & 2 deletions examples/serial/README.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -86,7 +86,7 @@ system file including client names and queue sizes, as well as updated initialis
for clients and virtualisers.
* **Makefile**
You must include directories for **SERIAL_COMPONENTS**, the **UART_DRIVER** and your
**SERIAL_CONFIG_INCLUDE**. You must also supply **SERIAL_NUM_CLIENTS**. You must add the uart
**SERIAL_CONFIG_INCLUDE**. You must also supply **NUM_SERIAL_CLIENTS**. You must add the uart
driver, transmit virtualiser and optionally the receive virtualiser to your image list. You must
add your serial include directory to your cflags, and finally you must include the uart driver
and serial_components make files. For each component you wish to have access to the serial
Expand Down Expand Up @@ -117,4 +117,4 @@ completed, and waits for input. When a character is received, each client will r
character using `sddf_putchar_unbuffered` which flushes the character to the device immediately. Every
tenth character each client will print a string containing their name using `sddf_printf` which
calls the serial `_sddf_putchar`, flushing characters to the device only when a `\n` is
encountered.
encountered.
Loading

0 comments on commit 9fe672d

Please sign in to comment.