[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [PVS] recommended platform

Adriaan de Groot writes:
   From: Adriaan de Groot <groot@kde.org>
   Date: Sat, 4 Jun 2005 21:39:37 +0200
   Subject: Re: [PVS] recommended platform
   On Saturday 04 June 2005 19:33, Nancy Griffeth wrote:
   > I know that Linux and Solaris platforms are supported, but what about
   This can be made more specific: Linux on x86 machines and Solaris on SPARC. 
   I'm not sure of the state of 32-bit support on Linux amd64; similarly, 

I run Pvs on a dual opteron system with Debian amd64. For running
32-bit applications I maintain a ia32 chroot, which contains the
necessary shared libraries. Most 32-bit application can be
started directly, ie. without using chroot or dchroot. 

After I deleted the LD_ASSUME_KERNEL line in the pvs shell script
also PVS runs without problems. That is, it uses the 64-bit
versions of emacs, wish and the other support tools, where the
lisp image runs in 32-bit legacy mode.

   Machine speed isn't critically important, 

My experience is completely different here: Also with medium size
specifications it can easily happen that you have to wait until
PVS finishes a proof command or until the proof tree catches up.
Not for hours, but it makes a difference if you have to wait 20
or 40 seconds until the smash finishes. Therefore I would always
by the fastest CPU available.

For a dual processor system: When rerunning proofs or when
developing large proofs often two applications need CPU time.
Either emacs and allegro-lisp or wish and allegro-lisp. That's
why I purchased a dual processor system. However, it did not
fulfil my expectations: emacs and allegro-lisp are often running
in parallel. However, they exploit their respective CPU's only to
60-70 percent. Both CPU's idle for the remaining time (20-30
percent). So the second CPU gives only a 30 percent speedup in
situations where it can be exploited (of course for typechecking
of bddsimp the second CPU doesn't help at all).