vprover/vampire

Reduce reliance on platform-specific APIs, improve Windows support

MichaelRawson opened this issue · 4 comments

Vampire should not need a great deal of platform-specific code. This is a tracking issue to remove as much as possible, and make what we absolutely need as cross-platform as we can.

We currently use platform-specific code:

  • for launching and monitoring processes in portfolio mode
  • for monitoring elapsed time
  • for monitoring used instructions
  • for semaphores used to synchronise portfolio processes
  • for our custom memory allocator
  • because we forgot to remove it

I'm currently looking at whether we can remove the memory allocator and the semaphores. Watch this space!

Using something akin to UNIX fork() is not really negotiable - we want to keep the existing Vampire state, notably the parsed problem, when we start a strategy - but it doesn't exist on Windows. We will have to rely on Cygwin for this on Windows, and hope that the various incompatibilities don't bite us.

Allocator is dead, long live Allocator! #469 removed the platform-specific code for allocation.

No more semaphores, no more semaphore support requirement.

Replacing global operator new portably to limit memory usage was so painful in the end (#592) that we gave up and call POSIX setrlimit in #594. Ho hum. Better POSIX than Linux.