Created
October 31, 2024 15:07
-
-
Save wolfspider/c6486b30e7a74beb87188c61ffc5f9e8 to your computer and use it in GitHub Desktop.
Formal Methods Ring Buffers
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| #include <stdio.h> | |
| #include <stdint.h> | |
| typedef struct t__int32_t_s | |
| { | |
| int32_t *b; | |
| uint32_t *first; | |
| uint32_t *length; | |
| uint32_t total_length; | |
| } | |
| t__int32_t; | |
| uint32_t next(uint32_t i, uint32_t total_length) | |
| { | |
| if (i == total_length - 1U) | |
| return 0U; | |
| else | |
| return i + 1U; | |
| } | |
| uint32_t prev(uint32_t i, uint32_t total_length) | |
| { | |
| if (i > 0U) | |
| return i - 1U; | |
| else | |
| return total_length - 1U; | |
| } | |
| uint32_t one_past_last(uint32_t i, uint32_t length, uint32_t total_length) | |
| { | |
| if (length == total_length) | |
| return i; | |
| else if (i >= total_length - length) | |
| return length - (total_length - i); | |
| else | |
| return i + length; | |
| } | |
| // Updated push to check for a full buffer using one_past_last | |
| void push__int32_t(t__int32_t x, int32_t e) | |
| { | |
| // Calculate the one past last index | |
| uint32_t one_past_last_index = one_past_last(*x.first, *x.length, x.total_length); | |
| if (*x.length < x.total_length) { // Not full, proceed normally | |
| uint32_t dest_slot = prev(*x.first, x.total_length); | |
| x.b[dest_slot] = e; | |
| *x.first = dest_slot; | |
| *x.length = *x.length + 1U; | |
| } else { // Buffer is full, overwrite the oldest element | |
| x.b[one_past_last_index] = e; | |
| *x.first = next(*x.first, x.total_length); | |
| } | |
| } | |
| int32_t pop__int32_t(t__int32_t x) | |
| { | |
| int32_t e = x.b[*x.first]; | |
| *x.first = next(*x.first, x.total_length); | |
| *x.length = *x.length - 1U; | |
| return e; | |
| } | |
| int32_t main(void) | |
| { | |
| int32_t b[3U]; | |
| for (uint32_t _i = 0U; _i < 3U; ++_i) | |
| b[_i] = (int32_t)1; | |
| uint32_t buf0 = 0U; | |
| uint32_t buf = 0U; | |
| t__int32_t rb = { .b = b, .first = &buf0, .length = &buf, .total_length = 3U }; | |
| push__int32_t(rb, (int32_t)10); | |
| push__int32_t(rb, (int32_t)20); | |
| push__int32_t(rb, (int32_t)30); | |
| push__int32_t(rb, (int32_t)40); // Overwrites oldest element | |
| int32_t r = pop__int32_t(rb); | |
| printf("out: %d\n", r); | |
| return r; | |
| } |
Author
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
The benefit to this approach is that this is easier to update with just sending an array of arbitrary bytes where a higher bound may exist with the number of slots before sending the payload. That functionality could be easily dropped in here. Now we can finally move on to a part 2 remaking this at a lower level.
A couple of edits to the code also brought speed up to this: