better shared memory handling?

[leofang]

If the GUI crashes very violently, it may be possible that the shared memory is not cleaned up. Try do a search (based on ownership) and clean up at GUI start time?

Challenges:

• this seems to work only for Linux (with /dev/shm)?

[leofang]

If the GUI crashes very violently, it may be possible that the shared memory is not cleaned up. Try do a search (based on ownership) and clean up at GUI start time?

Challenges:

• this seems to work only for Linux (with /dev/shm)?

feeea9c now does this. Question: Do we want to do an automatic cleanup at GUI start time, or let users do it at will to avoid potential interference with existing GUI processes? I incline the former, but wanna make sure this is safe.

[leofang]

Related: #41

[leofang]

potential interference with existing GUI processes

One such possibility is this: the user starts the GUI in a terminal and then runs a reconstruction, and in the meantime the user starts the GUI in another terminal. If we do the cleanup at start time, the shared memory of the first GUI will be wiped out by the second GUI. Got to think a clever way (without locking I hope)...

[leofang]

Related: 1d873d4

[leofang]

Related: #49