Shared memory ringbuffer based parser for proof hints (#1108)

This PR adds a shared memory ringbuffer based subclass for the
`proof_trace_buffer` abstract class that is used by the proof trace
parser to abstract away the mechanism in which the proof trace is being
read. The new subclass reads the proof trace from a ringbuffer located
in shared memory. In the future, we plan to add a corresponding writer
for the hint generator that will output the proof trace in the shared
memory ringbuffer. We do this in order to reduce the overhead of the
hint generation.

Some important notes/disclaimers for this PR:
- We use a typical producer/consumer synchronization scheme for
accessing the ringbuffer: we use two POSIX semaphores to singal data
available and space available. We assume only two processes, one reader
and one writer, and therefore we do not need to lock the accesses to the
buffer data.
- In order to test the new parser, we have added a new tool, namely
`kore-proof-trace-shm-writer`, that reads a proof trace file (the only
kind of output currently supported by the hint generator) and writes its
contents to the shared memory ringbuffer. In the future, we will add
support for the hint generator to opt to write the proof trace straight
into the ringbuffer, and at that point the `kore-proof-trace-shm-writer`
can be removed.
- The setup of the shared memory object and the initialization of the
semaphores happens in `kore-proof-trace` when it is passed a new flag,
namely `--shared-memory`. If the flag is passed then the `<input
filename>` positional argument serves as the name of the shared memory
object. The same name must be passed to `kore-proof-trace-shm-writer` in
order for the IPC to work. Moreover, the `kore-proof-trace-shm-writer`
invocation needs to allow some time for `kore-proof-trace` to finish the
setup. That is why we use `sleep 1` in CI between the two invocations.
- Currently, the reader and writer processes synchronize on reads/writes
of 1 byte. This is not very efficient and in a future PR we plan to add
support for buffered reads/writes of larger sizes. Note that the
ringbuffer API already can handle larger reads/writes.

The structure of the PR content is as follows:
- 2 new files, `include/kllvm/binary/ringbuffer.h` and
`lib/binary/ringbuffer.cpp`, contain the API and implementation for the
ringbuffer data structure.
- a new subclass of `proof_trace_buffer`, namely
`proof_trace_ringbuffer` is added to
`include/kllvm/binary/deserializer.h`. This subclass implements the
abstract API for various types of reads and peeks, all based on two
basic read and peek functions that contain the synchronization logic on
the reader's side.
- a new mode is added to the `tools/kore-proof-trace/main.cpp` program,
that does the setup of the shared memory object and the initialization
of the semaphores and invokes the shared memory/ringbuffer based hint
parser.
- a new tool is added in `tool/kore-proof-trace-shm-writer` that reads a
binary hint file and writes its contents to a provided shared memory
object. The tool contains the synchronization logic on the writer's
side.
- additional CI logic is added to `test/lit.cg.py` to allow parsing the
hint file with the new shared memory/ringbuffer based parser for all
tests that involve hint generation.

---------

Co-authored-by: Roberto Rosmaninho <[email protected]>
Co-authored-by: Bruce Collie <[email protected]>

Author: 3 people

include/kllvm/binary/ProofTraceParser.h

@@ -698,6 +698,8 @@ 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;

include/kllvm/binary/deserializer.h

@@ -2,12 +2,14 @@
 #define AST_DESERIALIZER_H
 
 #include <kllvm/ast/AST.h>
+#include <kllvm/binary/ringbuffer.h>
 #include <kllvm/binary/serializer.h>
 #include <kllvm/binary/version.h>
 
 #include <cstddef>
 #include <cstdio>
 #include <cstring>
+#include <deque>
 #include <fstream>
 #include <iostream>
 #include <vector>
@@ -203,6 +205,155 @@ 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_;
+  bool peek_eof_{false};
+  bool read_eof_{false};
+
+  bool read(uint8_t *ptr, size_t len = 1) {
+    for (size_t i = 0; i < len; i++) {
+      if (!peek_data_.empty()) {
+        ptr[i] = peek_data_.front();
+        peek_data_.pop_front();
+        continue;
+      }
+
+      if (peek_eof_) {
+        read_eof_ = true;
+        return false;
+      }
+
+      if (read_eof_) {
+        return false;
+      }
+
+      while (int wait_status = sem_trywait(data_avail_)) {
+        assert(wait_status == -1 && errno == EAGAIN);
+        if (shm_buffer_->eof()) {
+          read_eof_ = true;
+          return false;
+        }
+      }
+      shm_buffer_->get(&ptr[i]);
+      sem_post(space_avail_);
+    }
+
+    return true;
+  }
+
+  bool peek(uint8_t *ptr, size_t len = 1) {
+    for (size_t i = 0; i < len; i++) {
+      if (i < peek_data_.size()) {
+        ptr[i] = peek_data_[i];
+        continue;
+      }
+
+      if (peek_eof_) {
+        return false;
+      }
+
+      if (read_eof_) {
+        return false;
+      }
+
+      while (int wait_status = sem_trywait(data_avail_)) {
+        assert(wait_status == -1 && errno == EAGAIN);
+        if (shm_buffer_->eof()) {
+          peek_eof_ = true;
+          return false;
+        }
+      }
+      shm_buffer_->get(&ptr[i]);
+      sem_post(space_avail_);
+      peek_data_.push_back(ptr[i]);
+    }
+
+    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) {
+    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>

include/kllvm/binary/ringbuffer.h

@@ -0,0 +1,66 @@
+#ifndef RINGBUFFER_H
+#define RINGBUFFER_H
+
+#include <array>
+#include <cstdint>
+#include <cstdlib>
+#include <semaphore.h>
+
+namespace kllvm {
+
+// Simple ringbuffer class, intended to live in shared memory and operated by a
+// reader and a writer process.
+
+class shm_ringbuffer {
+public:
+  // Ringbuffer size in bytes.
+  // NOTE: In order to easily distinguish between when the buffer is full versus
+  // empty, we maintain the invariant that the capacity of the buffer is one byte
+  // less than its size. This way, the buffer is empty iff read_pos == write_pos,
+  // and it is full iff read_pos == (write_pos+1)%size.
+  static constexpr size_t size = 1024;
+
+  // Ringbuffer capacity in bytes.
+  // As commented above, the capacity is always equal to size-1.
+  static constexpr size_t capacity = size - 1;
+
+private:
+  bool eof_{false};
+  size_t read_pos_{0};
+  size_t write_pos_{0};
+  std::array<uint8_t, size> buffer_;
+
+public:
+  shm_ringbuffer();
+
+  ~shm_ringbuffer() = default;
+
+  // Returns the current size of the data contained in the ringbuffer.
+  [[nodiscard]] size_t data_size() const;
+
+  // Write EOF to the ring buffer. Further writes after this is called are
+  // undefined behavior.
+  void put_eof();
+
+  // Returns true when the ringbuffer is empty and the EOF has been written, and
+  // false otherwise. As commented above, the ringbuffer is empty iff
+  // read_pos == write_pos.
+  [[nodiscard]] bool eof() const;
+
+  // Add data to the ringbuffer. The behavior is undefined if the buffer does not
+  // have enough remaining space to fit the data or if EOF has been written to the
+  // ringbuffer. The behavior is also undefined if the data pointer passed to this
+  // function does not point to a contiguous memory chunk of the corresponding
+  // size.
+  void put(uint8_t const *data, size_t count = 1);
+
+  // Get and remove data from the ringbuffer. The behavior is undefined if more
+  // data is requested than it is currently available in the ringbuffer. The
+  // behavior is also undefined if the data pointer passed to this function does
+  // not point to a contiguous memory chunk of the corresponding size.
+  void get(uint8_t *data, size_t count = 1);
+};
+
+} // namespace kllvm
+
+#endif

lib/binary/CMakeLists.txt

@@ -2,6 +2,7 @@ add_library(BinaryKore
   serializer.cpp
   deserializer.cpp
   ProofTraceParser.cpp
+  ringbuffer.cpp
 )
 
 target_link_libraries(BinaryKore

lib/binary/ProofTraceParser.cpp

@@ -1,4 +1,5 @@
 #include <kllvm/binary/ProofTraceParser.h>
+#include <kllvm/binary/ringbuffer.h>
 
 #include <fmt/format.h>
 #include <fstream>
@@ -231,4 +232,22 @@ proof_trace_parser::parse_proof_trace_from_file(std::string const &filename) {
   return trace;
 }
 
+std::optional<llvm_rewrite_trace>
+proof_trace_parser::parse_proof_trace_from_shmem(
+    void *shm_object, sem_t *data_avail, sem_t *space_avail) {
+  proof_trace_ringbuffer buffer(shm_object, data_avail, space_avail);
+  llvm_rewrite_trace trace;
+  bool result = parse_trace(buffer, trace);
+
+  if (!result || !buffer.eof()) {
+    return std::nullopt;
+  }
+
+  if (verbose_) {
+    trace.print(std::cout, expand_terms_);
+  }
+
+  return trace;
+}
+
 } // namespace kllvm

lib/binary/ringbuffer.cpp

@@ -0,0 +1,82 @@
+#include <kllvm/binary/ringbuffer.h>
+
+#include <cassert>
+#include <cstring>
+
+namespace kllvm {
+
+shm_ringbuffer::shm_ringbuffer()
+    : buffer_() { }
+
+size_t shm_ringbuffer::data_size() const {
+  if (write_pos_ < read_pos_) {
+    return size - (read_pos_ - write_pos_);
+  }
+
+  return write_pos_ - read_pos_;
+}
+
+void shm_ringbuffer::put_eof() {
+  assert(!eof_);
+  eof_ = true;
+}
+
+bool shm_ringbuffer::eof() const {
+  // NOTE: for synchronization purposes, it is important that the eof_ field is
+  // checked first. Typically, the reader process will call this, so we want to
+  // avoid a race where the writer updates buf.writer_pos after the reader has
+  // accessed it but before the reader has fully evaluated the condition. If
+  // eof_ is checked first, and due to short-circuiting, we know that if eof_ is
+  // true, the writer will not do any further updates to the write_pos_ field,
+  // and if eof_ is false, the reader will not access write_pos_ at all.
+  return eof_ && write_pos_ == read_pos_;
+}
+
+void shm_ringbuffer::put(uint8_t const *data, size_t count) {
+  assert(!eof_);
+  assert(data);
+
+  // check if we need to wrap to the start of the ringbuffer
+  size_t no_wrap_size = size - write_pos_;
+  size_t rest_count = count;
+  if (count > no_wrap_size) {
+    // if yes, do a first copy to reach the end of the ringbuffer and wrap to
+    // start
+    memcpy(buffer_.data() + write_pos_, data, no_wrap_size);
+    write_pos_ = 0;
+    data += no_wrap_size;
+    rest_count = count - no_wrap_size;
+  }
+
+  // copy the (rest of the) data
+  memcpy(buffer_.data() + write_pos_, data, rest_count);
+  write_pos_ += rest_count;
+  if (write_pos_ == size) {
+    write_pos_ = 0;
+  }
+}
+
+void shm_ringbuffer::get(uint8_t *data, size_t count) {
+  assert(data);
+
+  // check if we need to wrap to the start of the ringbuffer
+  size_t no_wrap_size = size - read_pos_;
+  size_t rest_count = count;
+  if (count > no_wrap_size) {
+    // if yes, do a first copy to reach the end of the ringbuffer and wrap to
+    // start
+    memcpy(data, buffer_.data() + read_pos_, no_wrap_size);
+    read_pos_ = 0;
+    data += no_wrap_size;
+    rest_count = count - no_wrap_size;
+  }
+
+  // copy the (rest of the) data
+  memcpy(data, buffer_.data() + read_pos_, rest_count);
+  read_pos_ += rest_count;
+  if (read_pos_ == size) {
+    read_pos_ = 0;
+  }
+}
+
+} // namespace kllvm