Skip to content
GitLab
Commit 2d1ad898 authored by Michael Sammler's avatar Michael Sammler
Browse files

use spaces instead of tabs

parent d11a6083
Pipeline #65806 passed with stage
in 14 minutes and 26 seconds
Hide whitespace changes
Inline Side-by-side
.editorconfig
View file @ 2d1ad898
......@@ -6,3 +6,6 @@ insert_final_newline = true
[*.c]
indent_size = 2
[*.h]
indent_size = 2
examples/scheduler/include/fdsched.h
View file @ 2d1ad898
......@@ -7,12 +7,12 @@
/* state of the non-preemptive fixed-priority scheduler */
struct fd_scheduler {
/* the file descriptors we monitor */
struct pollfd input_channels[MAX_INPUT_CHANNELS];
nfds_t num_channels;
/* the file descriptors we monitor */
struct pollfd input_channels[MAX_INPUT_CHANNELS];
nfds_t num_channels;
/* the NP-FP scheduler */
struct npfp_scheduler sched;
/* the NP-FP scheduler */
struct npfp_scheduler sched;
};
......
examples/scheduler/include/fdsched/callback.h
View file @ 2d1ad898
......@@ -3,6 +3,6 @@
#include "fdsched/message.h"
struct callback {
priority_t prio;
int (*f)(struct message *msg);
priority_t prio;
int (*f)(struct message *msg);
};
examples/scheduler/include/fdsched/message.h
View file @ 2d1ad898
......@@ -19,20 +19,20 @@ typedef uint8_t message_type_t;
/* a message that was received via some input channel */
struct [[rc::parameters("cont : type")]]
[[rc::refined_by("data : message_data")]]
message {
[[rc::field("{m_type data} @ int<u8>")]]
message_type_t type;
[[rc::field("{m_length data} @ int<u64>")]]
size_t len;
[[rc::refined_by("data : message_data")]]
message {
[[rc::field("{m_type data} @ int<u8>")]]
message_type_t type;
[[rc::field("{m_length data} @ int<u64>")]]
size_t len;
/* embedded singly linked list of messages */
[[rc::field("cont")]]
struct message *next;
/* embedded singly linked list of messages */
[[rc::field("cont")]]
struct message *next;
#define MAX_MESSAGE_LEN (4096 - sizeof(message_type_t) - sizeof(size_t) - sizeof(struct message*))
[[rc::field("array<u8, {m_data data `at_type` int u8}>")]]
uint8_t data[MAX_MESSAGE_LEN];
[[rc::field("array<u8, {m_data data `at_type` int u8}>")]]
uint8_t data[MAX_MESSAGE_LEN];
};
/* interface: we expect the user to provide an implementation of this
......@@ -42,24 +42,24 @@ message_type_t message_identify_type(struct message* msg);
/* a simple FIFO queue of messages */
struct [[rc::refined_by("messages : {list message_data}")]]
[[rc::ptr_type("message_queue : ∃ p. own_constrained<tyown_constraint<p, null>, ...>")]]
message_queue {
[[rc::field("tyfold<{(λ data cont, &own (data @ message cont) : type) <$> messages}, place<p>>")]]
struct message *first;
[[rc::field("&own<place<p>>")]]
struct message **last;
[[rc::ptr_type("message_queue : ∃ p. own_constrained<tyown_constraint<p, null>, ...>")]]
message_queue {
[[rc::field("tyfold<{(λ data cont, &own (data @ message cont) : type) <$> messages}, place<p>>")]]
struct message *first;
[[rc::field("&own<place<p>>")]]
struct message **last;
};
/* enqueue at end */
[[rc::parameters("data : {list message_data}", "msg : message_data", "q : loc")]]
[[rc::args("q @ &own<data @ message_queue>",
"&own<msg @ message<uninit<void*>>>")]]
"&own<msg @ message<uninit<void*>>>")]]
[[rc::ensures("own q : {data ++ [msg]} @ message_queue")]]
static inline
void message_queue_add(struct message_queue *q, struct message *msg) {
msg->next = NULL;
*q->last = msg;
q->last = &msg->next;
msg->next = NULL;
*q->last = msg;
q->last = &msg->next;
}
......@@ -70,7 +70,7 @@ void message_queue_add(struct message_queue *q, struct message *msg) {
[[rc::ensures("own q : data @ message_queue")]]
static inline
int message_queue_empty(struct message_queue *q) {
return q->first == NULL;
return q->first == NULL;
}
/* dequeue from front */
......@@ -80,17 +80,17 @@ int message_queue_empty(struct message_queue *q) {
[[rc::ensures("own q : data @ message_queue")]]
static inline
struct message* message_queue_remove(struct message_queue *q) {
assert(!message_queue_empty(q));
assert(!message_queue_empty(q));
struct message* head = q->first;
struct message* head = q->first;
/* check if we're emptying the queue */
if (head->next == NULL) {
/* the queue is now empty */
q->first = NULL;
q->last = &q->first;
} else {
q->first = head->next;
}
return head;
/* check if we're emptying the queue */
if (head->next == NULL) {
/* the queue is now empty */
q->first = NULL;
q->last = &q->first;
} else {
q->first = head->next;
}
return head;
}
examples/scheduler/include/fdsched/priority.h
View file @ 2d1ad898
......@@ -14,7 +14,7 @@ typedef uint8_t priority_t;
/* a bitmap of "non-empty queue" indicators */
typedef struct {
uint64_t bits[4];
uint64_t bits[4];
} prio_bitmap_t;
typedef int priority_search_t;
......@@ -22,44 +22,44 @@ typedef int priority_search_t;
static inline
void prio_level_init(prio_bitmap_t *bm)
{
for(int lvl = 0; lvl < 4; lvl += 1) {
bm->bits[lvl] = 0;
}
for(int lvl = 0; lvl < 4; lvl += 1) {
bm->bits[lvl] = 0;
}
}
/* find the maximum priority level with pending work, or return -1 */
static inline
priority_search_t highest_pending_priority(prio_bitmap_t *bm) {
int offset = -1;
for (int i = 0; i < 4; i++) {
int first_bit = __builtin_ffsll(bm->bits[i]);
if (first_bit) {
return first_bit + offset;
} else {
offset += 64;
}
}
return -1;
int offset = -1;
for (int i = 0; i < 4; i++) {
int first_bit = __builtin_ffsll(bm->bits[i]);
if (first_bit) {
return first_bit + offset;
} else {
offset += 64;
}
}
return -1;
}
/* predicate: did we find a non-empty priority level? */
static inline
int priority_search_none_found(priority_search_t result) {
return result < 0;
return result < 0;
}
/* set the bit corresponding to the given priority */
static inline
void priority_level_set(prio_bitmap_t *bm, priority_t prio) {
uint8_t word = prio / 64;
uint8_t bit = prio % 64;
bm->bits[word] |= (((uint64_t) 1) << bit);
uint8_t word = prio / 64;
uint8_t bit = prio % 64;
bm->bits[word] |= (((uint64_t) 1) << bit);
}
/* clear the bit corresponding to the given priority */
static inline
void priority_level_clear(prio_bitmap_t *bm, priority_t prio) {
uint8_t word = prio / 64;
uint8_t bit = prio % 64;
bm->bits[word] &= ~(((uint64_t) 1) << bit);
uint8_t word = prio / 64;
uint8_t bit = prio % 64;
bm->bits[word] &= ~(((uint64_t) 1) << bit);
}
examples/scheduler/include/fdsched/priority_modified.h
View file @ 2d1ad898
......@@ -19,8 +19,8 @@ typedef struct
[[rc::refined_by("bitmap : Z")]]
[[rc::ptr_type("prio_bitmap_t : ... ")]]
{
[[rc::field("bitmap @ int<u64>")]]
uint64_t bits;
[[rc::field("bitmap @ int<u64>")]]
uint64_t bits;
} prio_bitmap_t;
typedef int priority_search_t;
......@@ -31,7 +31,7 @@ typedef int priority_search_t;
static inline
void prio_level_init(prio_bitmap_t *bm)
{
bm->bits = 0;
bm->bits = 0;
}
......@@ -43,12 +43,12 @@ void prio_level_init(prio_bitmap_t *bm)
[[rc::tactics("all: try by have := Z_least_significant_one_lower_bound bm; solve_goal.")]]
static inline
priority_search_t highest_pending_priority(prio_bitmap_t *bm) {
int offset = -1;
int first_bit = __builtin_ffsll(bm->bits);
if (first_bit != 0)
return first_bit -1;
else
return -1;
int offset = -1;
int first_bit = __builtin_ffsll(bm->bits);
if (first_bit != 0)
return first_bit -1;
else
return -1;
}
/* predicate: did we find a non-empty priority level? */
......@@ -57,7 +57,7 @@ priority_search_t highest_pending_priority(prio_bitmap_t *bm) {
[[rc::returns("{bool_decide (res < 0)} @ boolean<i32>")]]
static inline
int priority_search_none_found(priority_search_t result) {
return result < 0;
return result < 0;
}
/* set the bit corresponding to the given priority */
......@@ -68,7 +68,7 @@ int priority_search_none_found(priority_search_t result) {
[[rc::tactics("by apply Z_shiftl_1_range.")]]
static inline
void priority_level_set(prio_bitmap_t *bm, priority_t prio) {
bm->bits |= (((uint64_t) 1) << prio);
bm->bits |= (((uint64_t) 1) << prio);
}
/* clear the bit corresponding to the given priority */
......@@ -79,5 +79,5 @@ void priority_level_set(prio_bitmap_t *bm, priority_t prio) {
[[rc::lemmas("clearbit_equiv")]]
[[rc::tactics("by apply Z_shiftl_1_range.")]]
void priority_level_clear(prio_bitmap_t *bm, priority_t prio) {
bm->bits &= ~(((uint64_t) 1) << prio);
bm->bits &= ~(((uint64_t) 1) << prio);
}
examples/scheduler/include/fdsched/scheduler.h
View file @ 2d1ad898
......@@ -7,56 +7,56 @@
typedef int (*callback_fn_t)(struct message *);
struct callback {
priority_t prio;
callback_fn_t f;
priority_t prio;
callback_fn_t f;
};
/* state of the non-preemptive fixed-priority scheduler */
struct npfp_scheduler {
/* the registered callbacks */
struct callback callbacks[NUM_MESSAGE_TYPES];
/* the registered callbacks */
struct callback callbacks[NUM_MESSAGE_TYPES];
/* pending callback activations */
struct message_queue pending[NUM_PRIORITIES];
/* pending callback activations */
struct message_queue pending[NUM_PRIORITIES];
/* which priority levels are non-empty? */
prio_bitmap_t prio_levels;
/* which priority levels are non-empty? */
prio_bitmap_t prio_levels;
};
static inline
void npfp_enqueue(struct npfp_scheduler *sched, struct message* msg) {
/* identify the type of message we're looking at */
msg->type = message_identify_type(msg);
/* look up the fixed priority of such messages */
priority_t msg_prio = sched->callbacks[msg->type].prio;
/* add it to the appropriate queue */
message_queue_add(&sched->pending[msg_prio], msg);
/* note that the queue isn't empty anymore */
priority_level_set(&sched->prio_levels, msg_prio);
/* identify the type of message we're looking at */
msg->type = message_identify_type(msg);
/* look up the fixed priority of such messages */
priority_t msg_prio = sched->callbacks[msg->type].prio;
/* add it to the appropriate queue */
message_queue_add(&sched->pending[msg_prio], msg);
/* note that the queue isn't empty anymore */
priority_level_set(&sched->prio_levels, msg_prio);
}
static inline
struct message* npfp_dequeue(struct npfp_scheduler *sched) {
/* figure out top pending priority level */
int top_prio = highest_pending_priority(&sched->prio_levels);
if (priority_search_none_found(top_prio))
return NULL;
else {
/* dequeue the highest-priority message */
struct message *msg = message_queue_remove(&sched->pending[top_prio]);
/* check if we have to clear the priority bit */
if (message_queue_empty(&sched->pending[top_prio])) {
/* note that the queue is now empty */
priority_level_clear(&sched->prio_levels, top_prio);
}
return msg;
}
/* figure out top pending priority level */
int top_prio = highest_pending_priority(&sched->prio_levels);
if (priority_search_none_found(top_prio))
return NULL;
else {
/* dequeue the highest-priority message */
struct message *msg = message_queue_remove(&sched->pending[top_prio]);
/* check if we have to clear the priority bit */
if (message_queue_empty(&sched->pending[top_prio])) {
/* note that the queue is now empty */
priority_level_clear(&sched->prio_levels, top_prio);
}
return msg;
}
}
static inline
int npfp_dispatch(struct npfp_scheduler *sched, struct message *msg) {
return sched->callbacks[msg->type].f(msg);
return sched->callbacks[msg->type].f(msg);
}
examples/scheduler/include/sys/system.h
View file @ 2d1ad898
......@@ -5,18 +5,18 @@
#if defined(__refinedc__)
typedef int64_t ssize_t;
#define F_SETFL 4
#define O_NONBLOCK 04000
#define POLLIN 0x001
#define F_SETFL 4
#define O_NONBLOCK 04000
#define POLLIN 0x001
/* Type used for the number of file descriptors. */
typedef unsigned long int nfds_t;
/* Data structure describing a polling request. */
struct pollfd
{
int fd; /* File descriptor to poll. */
short int events; /* Types of events poller cares about. */
short int revents; /* Types of events that actually occurred. */
int fd; /* File descriptor to poll. */
short int events; /* Types of events poller cares about. */
short int revents; /* Types of events that actually occurred. */
};
// TODO: RefinedC does not understand ... so we use the concrete prototype that we use
......
examples/scheduler/src/fdsched.c
View file @ 2d1ad898
......@@ -7,131 +7,131 @@
static
int nop_callback(struct message* _) {
return 0;
return 0;
}
void fds_init(struct fd_scheduler* fds) {
fds->num_channels = 0;
// TODO: RefinedC currently does not accept the following:
/* fds->sched.prio_levels = (prio_bitmap_t) { 0 }; */
prio_level_init(&fds->sched.prio_levels);
for(int typ = 0; typ < NUM_MESSAGE_TYPES; typ += 1) {
fds->sched.callbacks[typ] = (struct callback) {0, nop_callback};
}
for(int prio = 0; prio < NUM_PRIORITIES; prio += 1) {
fds->sched.pending[prio] = (struct message_queue) {NULL, NULL};
}
fds->num_channels = 0;
// TODO: RefinedC currently does not accept the following:
/* fds->sched.prio_levels = (prio_bitmap_t) { 0 }; */
prio_level_init(&fds->sched.prio_levels);
for(int typ = 0; typ < NUM_MESSAGE_TYPES; typ += 1) {
fds->sched.callbacks[typ] = (struct callback) {0, nop_callback};
}
for(int prio = 0; prio < NUM_PRIORITIES; prio += 1) {
fds->sched.pending[prio] = (struct message_queue) {NULL, NULL};
}
}
int fds_add_channel(struct fd_scheduler* fds, int fd) {
assert(fds->num_channels < MAX_INPUT_CHANNELS);
assert(fds->num_channels < MAX_INPUT_CHANNELS);
/* mark as nonblocking */
int err = fcntl(fd, F_SETFL, O_NONBLOCK);
if (err)
return err;
/* mark as nonblocking */
int err = fcntl(fd, F_SETFL, O_NONBLOCK);
if (err)
return err;
fds->input_channels[fds->num_channels].fd = fd;
fds->input_channels[fds->num_channels].events = POLLIN;
fds->num_channels++;
fds->input_channels[fds->num_channels].fd = fd;
fds->input_channels[fds->num_channels].events = POLLIN;
fds->num_channels++;
return 0;
return 0;
}
void fds_set_callback(struct fd_scheduler* fds,
message_type_t type, callback_fn_t f, priority_t prio) {
fds->sched.callbacks[type] = (struct callback) {prio, f};
message_type_t type, callback_fn_t f, priority_t prio) {
fds->sched.callbacks[type] = (struct callback) {prio, f};
}
static
void wait_for_input(struct fd_scheduler* fds) {
int err;
int err;
/* Wait for data to become available, ignoring spurious
wake-ups due to signals. */
do {
err = poll(fds->input_channels, fds->num_channels, -1);
} while (err < 0);
/* Wait for data to become available, ignoring spurious
wake-ups due to signals. */
do {
err = poll(fds->input_channels, fds->num_channels, -1);
} while (err < 0);
}
static
int receive_one_message(struct fd_scheduler* fds, int fd) {
/* NB: we really should use pre-allocated memory here to avoid page faults */
struct message *msg = malloc(sizeof(*msg));
/* we are not going to handle memory allocation failures */
assert(msg);
/* receive data from FD */
int n = read(fd, &msg->data, MAX_MESSAGE_LEN);
if (n <= 0) {
// FIXME: should handle closed FDs gracefully
free(msg);
return n;
} else {
msg->len = n;
npfp_enqueue(&fds->sched, msg);
return 0;
}
/* NB: we really should use pre-allocated memory here to avoid page faults */
struct message *msg = malloc(sizeof(*msg));
/* we are not going to handle memory allocation failures */
assert(msg);
/* receive data from FD */
int n = read(fd, &msg->data, MAX_MESSAGE_LEN);
if (n <= 0) {
// FIXME: should handle closed FDs gracefully
free(msg);
return n;
} else {
msg->len = n;
npfp_enqueue(&fds->sched, msg);
return 0;
}
}
static
int receive_messages(struct fd_scheduler* fds, int fd) {
int err;
do {
err = receive_one_message(fds, fd);
} while (!err);
if (errno == EWOULDBLOCK || errno == EAGAIN)
/* nothing else to receive for now, this is fine */
return 0;
else
return err;
int err;
do {
err = receive_one_message(fds, fd);
} while (!err);
if (errno == EWOULDBLOCK || errno == EAGAIN)
/* nothing else to receive for now, this is fine */
return 0;
else
return err;
}
static
int check_channels(struct fd_scheduler* fds) {
int err;
for (nfds_t ch = 0; ch < fds->num_channels; ch++) {
if (fds->input_channels[ch].revents) {
err = receive_messages(fds, fds->input_channels[ch].fd);
if (err < 0)
return err;
}
}
return 0;
int err;
for (nfds_t ch = 0; ch < fds->num_channels; ch++) {
if (fds->input_channels[ch].revents) {
err = receive_messages(fds, fds->input_channels[ch].fd);
if (err < 0)
return err;
}
}
return 0;
}
int fds_run(struct fd_scheduler* fds) {
int err;
int err;
assert(fds->num_channels > 0);
assert(fds->num_channels > 0);
while (1) {
wait_for_input(fds);
do {
/* receive messages on all channels */
err = check_channels(fds);
if (err)
return err;
while (1) {
wait_for_input(fds);
do {
/* receive messages on all channels */
err = check_channels(fds);
if (err)
return err;
/* get the highest-priority message */
struct message *msg = npfp_dequeue(&fds->sched);
/* get the highest-priority message */
struct message *msg = npfp_dequeue(&fds->sched);
/* if there is no message, wait for new input */
if (!msg)
break;
/* if there is no message, wait for new input */
if (!msg)
break;
/* consume the message */
err = npfp_dispatch(&fds->sched, msg);
/* consume the message */
err = npfp_dispatch(&fds->sched, msg);