| <!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.0 Transitional//EN"> |
| |
| <html> |
| <head> |
| <link rel="stylesheet" type="text/css" href="help.css"> |
| <title>GEM - Preferences</title> |
| </head> |
| |
| <body> |
| <a name="top"></a> |
| <table cellspacing="5"> |
| <tr> |
| <td> |
| <img src="images/trident_transparent.png"> |
| </td> |
| <td> |
| <h1>GEM - Preferences</h1> |
| </td> |
| </tr> |
| </table> |
| |
| <hr> |
| |
| <p> |
| <em>To edit preferences, from the Eclipse menus, go to <b>Window -> Preferences -> Parallel Tools -> GEM</b></em> |
| </p> |
| |
| <p> |
| GEM has two preference pages: |
| </p> |
| <ol> |
| <li> |
| <b>GEM Preferences:</b> 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). |
| </li> |
| <li> |
| <b>ISP Preferences:</b> This preference page is for command line settings for the underlying formal |
| verification engine GEM uses, In-situ Parital Order (ISP) |
| </li> |
| </ol> |
| |
| <h4>Below are detailed descriptions of each of GEM's Preference Pages.</h4> |
| |
| <hr/> |
| |
| <h2><a name="gemprefs">GEM Preference Page</a></h2> |
| <br/> |
| <a name="gemPrefs"></a> |
| <img src="images/gemPrefs.png"> |
| |
| <h4>Note:</h4> |
| <ol> |
| <li> |
| 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. |
| </li> |
| </ol> |
| |
| <h3>GEM Preferences Reference Table</h3> |
| <table border="1" cellpadding="5"> |
| <tr><th>Preference</th><th>Meaning or Condition When Selected</th></tr> |
| <tr> |
| <td>Number of Processes:</td> |
| <td> |
| 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 |
| <a href="setNumProcs.html">Setting the Number of Processes</a> page. |
| </td> |
| </tr> |
| <tr> |
| <td>Clear GEM Console on Each Run</td> |
| <td> |
| 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). |
| </td> |
| </tr> |
| <tr> |
| <td>Request Command Line Arguments</td> |
| <td> |
| 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. |
| </td> |
| </tr> |
| <tr> |
| <td>Active View:</td> |
| <td> |
| 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". |
| </td> |
| </tr> |
| </table> |
| |
| <br/> |
| <hr/> |
| |
| <h2>ISP Preference Page</h2> |
| <br/> |
| <a name="ispPrefs"></a> |
| <img src="images/ispPrefs.png"> |
| |
| <h4>Note:</h4> |
| <ol> |
| <li> |
| 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 (<tt><b>/usr/local/bin</b></tt>). |
| These items simply need to be in your path (we show <tt><b>/usr/local/bin</b></tt> purely for the sake of illustration here). |
| </li> |
| <li> |
| 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. |
| </li> |
| </ol> |
| |
| <h3>ISP Preferences Reference Table</h3> |
| <table border="1" cellpadding="8"> |
| <tr><th colspan="2">Command Line Options</th></tr> |
| <tr><td>Enable FIB</td> <td>Enables detection of irrelevant barriers</td></tr> |
| <tr><td>Log Total MPI Calls</td> <td>Outputs the number of MPI calls trapped for each rank (Console View)</td></tr> |
| <tr><td>Enable OpenMP</td> <td>Enables OpenMP based parallelization on multi-core machines</td></tr> |
| <tr><td>Use Blocking Sends</td> <td>Sends will be treated as blocking, without buffering</td></tr> |
| <tr><td>Report Progress</td> <td>Outputs progress every (n) MPI calls (default is 4). Note: If this is checked, please set the Report progress field below</td></tr> |
| <tr><td>Use Unix Sockets</td> <td>Enable this when running GEM on a single, local machine. It speeds up ISP/GEM significantly</td></tr> |
| <tr><td>Verbose Mode</td> <td>Output the transition list for all interleavings, otherwise only output last interleaving if deadlock.</td></tr> |
| <tr><th colspan="2">Miscellaneous Options</th></tr> |
| <tr><td>Port</td> <td>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</td></tr> |
| <tr><td>Report Progress Every (n) MPI Calls</td> <td>Outputs progress every (n) MPI calls (default is 4). Note: This is ignored if Report Progress is not checked</td></tr> |
| <tr><td>Host Where ISP Resides</td> <td>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</td></tr> |
| <tr><th colspan="2">ISP Paths</th></tr> |
| <tr><td>isp executable </td> <td>The location of the local <b>isp executable</b> (this is ISP itself)</td></tr> |
| <tr><td>ispcc script</td> <td>The location of the local <b>ispcc script</b> (for C compilation)</td></tr> |
| <tr><td>ispCC script</td> <td>The location of the local <b>ispCC script</b> (for C++ compilation)</td></tr> |
| <tr><td>HB Viewer script</td> <td>The location of the <b>HB Viewer</b> script (a.k.a. ispUI). This will only be local.</td></tr> |
| <tr><td>remote isp executable </td> <td>The location of the remote <b>isp executable</b> (this is ISP itself)</td></tr> |
| <tr><td>remote ispcc script</td> <td>The location of the remote <b>ispcc script</b> (for C compilation)</td></tr> |
| <tr><td>remote ispCC script</td> <td>The location of the remote <b>ispCC script</b> (for C++ compilation)</td></tr> |
| </table> |
| |
| <br/><br/> |
| <p><a href="#top">Back to Top</a> | <a href="toc.html">Back to Table of Contents</a></p> |
| <br/><br/> |
| |
| <hr/> |
| |
| <center> |
| <p> |
| School of Computing * 50 S. Central Campus Dr. Rm. 3190 * Salt Lake City, UT |
| 84112 * <A href="mailto:isp-dev@cs.utah.edu">isp-dev@cs.utah.edu</a><br> |
| <a href="http://www.eclipse.org/org/documents/epl-v10.php">License</a> |
| </p> |
| </center> |
| |
| </body> |
| </html> |
