Skip to content

Commit

Permalink
Removing shared memory proof trace reader/writer (#1132)
Browse files Browse the repository at this point in the history 
We measured the performance of the shared memory implementation for
reading and writing proof traces and it turns out it does not provide
significant benefits compared to using the file system. For this reason,
this PR removes the relevant code so that we don't have to maintain it.
  • Loading branch information
@theo25
theo25 authored Aug 9, 2024
1 parent e098717 commit c202d7c
Show file tree
Hide file tree
Showing 73 changed files with 3 additions and 936 deletions.
2 changes: 0 additions & 2 deletions include/kllvm/binary/ProofTraceParser.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -698,8 +698,6 @@ class proof_trace_parser {

std::optional<llvm_rewrite_trace>
parse_proof_trace_from_file(std::string const &filename);
std::optional<llvm_rewrite_trace> parse_proof_trace_from_shmem(
void *shm_object, sem_t *data_avail, sem_t *space_avail);
std::optional<llvm_rewrite_trace> parse_proof_trace(std::string const &data);

friend class llvm_rewrite_trace_iterator;
Expand Down
255 changes: 0 additions & 255 deletions include/kllvm/binary/deserializer.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,6 @@
#define AST_DESERIALIZER_H

#include <kllvm/ast/AST.h>
#include <kllvm/binary/ringbuffer.h>
#include <kllvm/binary/serializer.h>
#include <kllvm/binary/version.h>

Expand Down Expand Up @@ -205,260 +204,6 @@ class proof_trace_file_buffer : public proof_trace_buffer {
}
};

class proof_trace_ringbuffer : public proof_trace_buffer {
private:
shm_ringbuffer *shm_buffer_;
sem_t *data_avail_;
sem_t *space_avail_;

std::deque<uint8_t> peek_data_;
std::array<uint8_t, shm_ringbuffer::buffered_access_sz> buffer_;
size_t buffer_data_size_{0};
size_t buffer_data_start_{0};

bool peek_eof_{false};
bool buffered_eof_{false};
bool read_eof_{false};

// Helper function that reads from the shared memory ringbuffer into the
// buffer_. It tries to read shm_ringbuffer::buffered_access_sz bytes of data.
// It assumes that buffer_ is empty.
void read_from_shared_memory() {
assert(buffer_data_size_ == 0);
assert(buffer_data_start_ == 0);

if (buffered_eof_) {
return;
}

sem_wait(data_avail_);

if (shm_buffer_->eof()) {
// EOF has been written to the ringbuffer. Check if this is the last chunk
// of data to be read.
size_t remaining_data_sz = shm_buffer_->data_size();
if (remaining_data_sz < shm_ringbuffer::buffered_access_sz) {
// This is the last chunk of data to be read from the ringbuffer.
shm_buffer_->get(buffer_.data(), remaining_data_sz);
sem_post(space_avail_);

buffer_data_size_ = remaining_data_sz;
buffered_eof_ = true;

return;
}
}

// Else, either EOF has not been written or EOF has been written but there
// are remaining full chunks to be read. In any case, we can read a full
// chunk.
shm_buffer_->get(buffer_.data());
sem_post(space_avail_);

buffer_data_size_ = shm_ringbuffer::buffered_access_sz;
}

bool read(uint8_t *ptr, size_t len = 1) {
// Check if we have read EOF already.
if (read_eof_) {
return false;
}

// Consume peeked data.
while (len > 0 && !peek_data_.empty()) {
*ptr = peek_data_.front();
peek_data_.pop_front();
ptr++;
len--;
}

// Consume peeked EOF.
if (len > 0 && peek_eof_) {
read_eof_ = true;
return false;
}

// Peeked data has been fully consumed. If more data is requested, we need
// to read from buffer_ and/or shared memory.
while (len > 0) {
// If buffer_ is empty, try to fetch more data from the shared memory
// ringbuffer.
if (buffer_data_size_ == 0) {
// Check for and conusme buffered EOF.
if (buffered_eof_) {
read_eof_ = true;
return false;
}

assert(buffer_data_start_ == 0);
read_from_shared_memory();
}

// Read available data from the buffer_.
assert(buffer_data_start_ < shm_ringbuffer::buffered_access_sz);
assert(
buffer_data_start_ + buffer_data_size_
<= shm_ringbuffer::buffered_access_sz);
size_t size_to_read_from_buffer = std::min(len, buffer_data_size_);
memcpy(
ptr, buffer_.data() + buffer_data_start_, size_to_read_from_buffer);
ptr += size_to_read_from_buffer;
len -= size_to_read_from_buffer;

buffer_data_start_ += size_to_read_from_buffer;
buffer_data_size_ -= size_to_read_from_buffer;
if (buffer_data_start_ == shm_ringbuffer::buffered_access_sz) {
assert(buffer_data_size_ == 0);
buffer_data_start_ = 0;
}
}

assert(len == 0);
return true;
}

bool peek(uint8_t *ptr, size_t len = 1) {
// Check if we have read EOF already.
if (read_eof_) {
return false;
}

// Copy already peeked data.
size_t i = 0;
while (len > 0 && i < peek_data_.size()) {
*ptr = peek_data_[i];
ptr++;
i++;
len--;
}

// Check for already peeked EOF.
if (len > 0 && peek_eof_) {
return false;
}

// Already peeked data has been fully copied. If more data is requested, we
// need to peek from buffer_ and/or shared memory.
while (len > 0) {
// If buffer_ is empty, try to fetch more data from the shared memory
// ringbuffer.
if (buffer_data_size_ == 0) {
// Check for buffered EOF.
if (buffered_eof_) {
peek_eof_ = true;
return false;
}

assert(buffer_data_start_ == 0);
read_from_shared_memory();
}

// Peek available data from the buffer_.
assert(buffer_data_start_ < shm_ringbuffer::buffered_access_sz);
assert(
buffer_data_start_ + buffer_data_size_
<= shm_ringbuffer::buffered_access_sz);
size_t size_to_peek_from_buffer = std::min(len, buffer_data_size_);
memcpy(
ptr, buffer_.data() + buffer_data_start_, size_to_peek_from_buffer);
peek_data_.insert(
peek_data_.end(), buffer_.begin() + buffer_data_start_,
buffer_.begin() + buffer_data_start_ + size_to_peek_from_buffer);
ptr += size_to_peek_from_buffer;
len -= size_to_peek_from_buffer;

buffer_data_start_ += size_to_peek_from_buffer;
buffer_data_size_ -= size_to_peek_from_buffer;
if (buffer_data_start_ == shm_ringbuffer::buffered_access_sz) {
assert(buffer_data_size_ == 0);
buffer_data_start_ = 0;
}
}

assert(len == 0);
return true;
}

public:
proof_trace_ringbuffer(
void *shm_object, sem_t *data_avail, sem_t *space_avail)
: shm_buffer_(static_cast<shm_ringbuffer *>(shm_object))
, data_avail_(data_avail)
, space_avail_(space_avail)
, buffer_() {
new (shm_buffer_) shm_ringbuffer;
}

~proof_trace_ringbuffer() override { shm_buffer_->~shm_ringbuffer(); }

proof_trace_ringbuffer(proof_trace_ringbuffer const &) = delete;
proof_trace_ringbuffer(proof_trace_ringbuffer &&) = delete;
proof_trace_ringbuffer &operator=(proof_trace_ringbuffer const &) = delete;
proof_trace_ringbuffer &operator=(proof_trace_ringbuffer &&) = delete;

bool read(void *ptr, size_t len) override {
auto *data = static_cast<uint8_t *>(ptr);
return read(data, len);
}

int read() override {
uint8_t c = 0;
if (read(&c)) {
return c;
}
return -1;
}

bool has_word() override {
uint64_t word = 0;
auto *data = reinterpret_cast<uint8_t *>(&word);
return peek(data, sizeof(word));
}

bool eof() override { return peek() == -1; }

int peek() override {
uint8_t c = 0;
if (peek(&c)) {
return c;
}
return -1;
}

uint64_t peek_word() override {
uint64_t word = 0;
auto *data = reinterpret_cast<uint8_t *>(&word);
if (!peek(data, sizeof(word))) {
assert(false);
}
return word;
}

bool read_uint32(uint32_t &i) override { return read(&i, sizeof(i)); }

bool read_uint64(uint64_t &i) override { return read(&i, sizeof(i)); }

bool read_string(std::string &str) override {
str.resize(0);
while (true) {
int c = read();
if (c == -1) {
return false;
}
if ((char)c == '\0') {
break;
}
str.push_back((char)c);
}
return true;
}

bool read_string(std::string &str, size_t len) override {
str.resize(len);
return read(str.data(), len);
}
};

namespace detail {

template <typename It>
Expand Down
69 changes: 0 additions & 69 deletions include/kllvm/binary/ringbuffer.h
View file

This file was deleted.

36 changes: 0 additions & 36 deletions include/kllvm/binary/serializer.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,6 @@
#define AST_SERIALIZER_H

#include <kllvm/ast/AST.h>
#include <kllvm/binary/ringbuffer.h>
#include <kllvm/binary/version.h>

#include <array>
Expand Down Expand Up @@ -182,41 +181,6 @@ class proof_trace_file_writer : public proof_trace_writer {
void write_eof() override { }
};

class proof_trace_ringbuffer_writer : public proof_trace_writer {
private:
shm_ringbuffer *shm_buffer_;
sem_t *data_avail_;
sem_t *space_avail_;

std::array<uint8_t, shm_ringbuffer::buffered_access_sz> buffer_;
size_t buffer_data_size_{0};

void write(uint8_t const *ptr, size_t len = 1);

public:
proof_trace_ringbuffer_writer(
void *shm_object, sem_t *data_avail, sem_t *space_avail)
: shm_buffer_(reinterpret_cast<shm_ringbuffer *>(shm_object))
, data_avail_(data_avail)
, space_avail_(space_avail)
, buffer_() { }

~proof_trace_ringbuffer_writer() override { shm_buffer_->~shm_ringbuffer(); }

proof_trace_ringbuffer_writer(proof_trace_ringbuffer_writer const &) = delete;
proof_trace_ringbuffer_writer(proof_trace_ringbuffer_writer &&) = delete;
proof_trace_ringbuffer_writer &
operator=(proof_trace_ringbuffer_writer const &)
= delete;
proof_trace_ringbuffer_writer &operator=(proof_trace_ringbuffer_writer &&)
= delete;

void write(void const *ptr, size_t len) override;
void write_string(char const *str, size_t len) override;
void write_string(char const *str) override;
void write_eof() override;
};

} // namespace kllvm

#endif
Loading

0 comments on commit c202d7c

Please sign in to comment.