Some notes on ELF 🧝 loading and dynamic linking mainly for GNU userland
(ld.so, libc, libdl) running on top of the Linux kernel. Some
prior knowlegde on the topic (virtual memory, shared objects,
sections) might be useful to understand this.
In an attempt to simplify the development around the SimGrid
model-checker, we were thinking about moving the model-checker out in
a different process. Another different approach would be to use a
dynamic-linker isolation of the different components of the process.
Here is a summary of the goals, problems and design issues surrounding
these topics.
In the previous episode, I talked about the
implementation of a same-page-merging page store. On top of this, we
can build same-page-merging snapshots for the SimGrid model checker.
The first (lower) layer of the per-page snapshot mechanism is a page
store: its responsibility is to store immutable shareable
reference-counted memory pages independently of the snapshoting
logic. Snapshot management and representation, soft-dirty tracking
will be handled in higher layer.
Per-page shallow snapshots for the SimGrid model checker
Published:
I looked at my options to achieve efficient/cheap snapshots of the
simulated application for the Simgrid model checker using
copy-on-write. Here I look at another
solution to achieve this without using copy-on-write.
Copy-on-write snapshots for the SimGrid model checker
Published:
The SimGrid model checker
explores the graph of possible executions of
a simulated distributed application in order to verify safety and
liveness properties. The model checker needs to store the state of the
application in each node of the execution graph in order to detect
cycles. However, saving the whole state of the application at each
node of the graph leads to huge memory consumption and in some
cases most of the time is spent copying data in order to take the
snapshots of the application. We will see how we could solve this problem,
using copy-on-write.