Shared memory ringbuffer based parser for proof hints

[theo25]

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.

[Robertorosmaninho]

The PR, so far LGTM! I couldn’t spot why it’s failing in macOS, though, so I think this is the last thing needed to merge this PR.

I would like to see if it’s possible to have a more C++ style for the ringbuffer definition in the future. We should also have some Python bindings to expose this to MPG. The code was very well inline-documented, and the PR description helped a lot during the review.

Thanks for your hard work on this!

[gtrepta]

LGTM, and works on my machine.

[Baltoli]

I left a couple of suggestions for the internal data structure that would let you improve the code quality a little, but feel free to stick with your current implementation if you'd rather.

[theo25]

I have managed to fix the issues with MacOS. There were 2 main issues:

• As far as I can tell, MacOS does not support combining O_TRUNC with O_CREAT | O_EXCL in shm_open.
• More importantly, the unnamed POSIX semaphores are not supported in MacOS. For that reason, I am using named semaphores. Another complication is that the names used for named semaphores in MacOS cannot exceed 32 characters in length. To accommodate that, and still have different names for semaphores of different tests (required since tests can run in parallel), I had to make some brevity changes in the naming convection for these semaphores.

[Robertorosmaninho]

@theo25, if you're confident that this PR is ready to merge, go ahead and merge it. We can deal with the C++ style later, just create an issue for that. That's a low priority atm.

[Robertorosmaninho]

Thanks for addressing our comments. LGTM!