GEM - Preferences


To edit preferences, from the Eclipse menus, go to Window -> Preferences -> Parallel Tools -> GEM

GEM has two preference pages:

  1. GEM Preferences: This preference page is for settings related to how views and various components within GEM behave and function. Here the user can control which GEM Views are shown and when, e.g. the active view (the view in focus after verification is complete).
  2. ISP Preferences: This preference page is for command line settings for the underlying formal verification engine GEM uses, In-situ Parital Order (ISP)

Below are detailed descriptions of each of GEM's Preference Pages.


GEM Preference Page


Note:

  1. Please note the smaller help button on this preference page (below the "Active View:" label). Clicking this button while viewing the GEM preference page will bring you to this help page.

GEM Preferences Reference Table

PreferenceMeaning or Condition When Selected
Number of Processes: This field takes an integer value that represents the number of processes to use for the next GEM verification. It is what is stored after going through the motions on the Setting the Number of Processes page.
Clear GEM Console on Each Run When enabled (checked), the GEM Console will be cleared prior to each verification run. If this preference is not enabled, output is appended to the existing GEM Console content (at the bottom).
Request Command Line Arguments When enabled (checked), a dialog box will appear when GEM verification is started. This dialog box will ask for command line arguments. When disabled, no dialog box will appear.
Verify ISP Output Consistency This is really a tool meant for internal development. It is suggested that you keep this preference disabled.
Active View: The selected view will be the one that gets the active focus after each GEM verification run, e.g. if you would like to see the Analyzer View after each verification, then simply select "Analyzer".


ISP Preference Page


Note:

  1. If ISP is configured and installed with default values, there is no need to fill in the four items in the "ISP Paths" group of the ISP preferences page. When blank, the plug-in will assume they are in the default location (/usr/local/bin). These items simply need to be in your path (we show /usr/local/bin purely for the sake of illustration here).
  2. Please note the smaller help button on this preference page (below "ISP Paths" group). Clicking this button while viewing the ISP preference page will bring you to this help page.

ISP Preferences Reference Table

Command Line Options
Enable FIB Enables detection of irrelevant barriers
Log Total MPI Calls Outputs the number of MPI calls trapped for each rank (Console View)
Enable OpenMP Enables OpenMP based parallelization on multi-core machines
Use Blocking Sends Sends will be treated as blocking, without buffering
Report Progress Outputs progress every (n) MPI calls (default is 4). Note: If this is checked, please set the Report progress field below
Use Unix Sockets Enable this when running GEM on a single, local machine. It speeds up ISP/GEM significantly
Verbose Mode Output the transition list for all interleavings, otherwise only output last interleaving if deadlock.
Miscellaneous Options
Port Assigns the port to communicate with MPI programs(default is 9999). GEM will search for a port that is free if specified port is unavailable
Report Progress Every (n) MPI Calls Outputs progress every (n) MPI calls (default is 4). Note: This is ignored if Report Progress is not checked
Host Where ISP Resides If ISP is installed on a remote machine, enter the fully qualified hostname here. If ISP is installed on your local machine (e.g. laptop), leave this blank
ISP Paths
isp executable The location of the local isp executable (this is ISP itself)
ispcc script The location of the local ispcc script (for C compilation)
ispCC script The location of the local ispCC script (for C++ compilation)
HB Viewer script The location of the HB Viewer script (a.k.a. ispUI). This will only be local.
remote isp executable The location of the remote isp executable (this is ISP itself)
remote ispcc script The location of the remote ispcc script (for C compilation)
remote ispCC script The location of the remote ispCC script (for C++ compilation)


Back to Top | Back to Table of Contents




School of Computing * 50 S. Central Campus Dr. Rm. 3190 * Salt Lake City, UT 84112 * isp-dev@cs.utah.edu
License