analyzer icon indicating copy to clipboard operation
analyzer copied to clipboard

Process-level concurrency and shared memory

Open sim642 opened this issue 3 years ago • 0 comments

While looking at chrony and how it uses a pipe to return results from a pthread thread (which is a bit weird in itself), I remembered the pre-threads way of achieving concurrency: fork a process, which yields two processes (a parent and a child, based on the return value), which continue executing the same program concurrently (although usually they're made to run different logic based on the fork return value). As of now, Goblint is oblivious to this form of concurrency.

This in itself isn't too big of a problem because the parent and child process run in separate memory spaces, so luckily values of global variables are not shared between the two. However, there are exceptions to that rule:

  1. mmap can be used to allocate memory, which remains shared by the processes. For example: https://stackoverflow.com/a/13274800/854540.
  2. shmget and shmat can be used to specifically work with memory shared by processes. For example, refclock_shm.c in chrony uses this mechanism for something.

I'd say this isn't something that we urgently need Goblint to support, because compared to pthread, I imagine it's even rarer (at least nowadays) to use the above mechanisms. Nevertheless, it might be something to keep in mind when trying to analyze old Posix programs. Or it might be something obscure for a student to try to tackle.

sim642 avatar Apr 29 '22 07:04 sim642