Let's get started.

Instructions to download and install GameTime.

Downloading

The current version of GameTime is 1.5 (released July 2015, download size: 115 MB). The previous version is also available (version 1.0, released June 2014, download size: 115MB). Version 1.5 adds new feature called overcomplete basis described in Tutorial 4 on the tutorials page.

Download GameTime 1.5 Download GameTime 1.0

To install GameTime, download and follow the installation instructions.

To update GameTime, download and follow step 4 and step 5 of the installation instructions.

GameTime is currently only available for Microsoft Windows. Efforts are currently underway to make it available for other operating systems. If you would like to contribute to GameTime as a developer, please contact us.

Version History

Version 1.0 (released June 2, 2014): Initial release of GameTime.

Unsupported Code Constructs

The list below details the code constructs that are not completely supported by the latest version of GameTime. Better support is planned and scheduled for future versions.

  • Floating-point values are rounded down to the nearest integer.
  • Global initializers that use ternary expressions and floating-point values are not supported.
  • Numeric memory addresses are not supported.
  • Pointer assignment and pointer comparison are not completely supported.

If you notice that GameTime is unable to deal with a code construct not listed above, please contact us with information about the code construct and, preferably, a sample.

Installation

If you run into any issues during installation, please contact us and we will respond as soon as possible.

Step 1: Installation of Software

  1. Install the 32-bit version of Cygwin. During the Cygwin installation process, you will be asked to select packages to install. Select at least the following packages:

    • automake
    • gcc-core
    • glpk
    • make
    • patch
    • perl
    • coreutils (Recommended, but not required.)
    • ncurses (Recommended, but not required.)

  2. Install the 32-bit version of Python. The recommended version of Python is 2.7.6.

    Cygwin has a version of Python that is insufficient for GameTime, so Python needs to be installed separately.

  3. Install either Microsoft Visual Studio 2008 or Microsoft Visual C++ Express 2008.
    If you do not have a copy of either, but you are a student or a staff member at an academic institution, you may be able to use Microsoft DreamSpark, which allows the download of Microsoft Visual C++ Express 2008.

  4. Install Microsoft Phoenix, the infrastructure for program analysis and transformation from Microsoft. We have provided a copy of the installer with the name Phoenix-SDK-June-2008-RC1.msi, located in the directory ext.

Step 2: Configuration of SMT Solver and ILP Solver

GameTime uses an SMT (satisfiability modulo theories) solver and an ILP (integer linear programming) solver as part of its workflow. It thus expects the paths to an SMT solver and to an ILP solver to be available in the PATH system variable. (To learn about how to add a path to the PATH system variable, refer to the appendix.)

At least one of these SMT solvers must be installed and available:

  • Boolector: Once configured and installed, add the path for the Boolector executable (boolector.exe) to the PATH system variable. Additionally, GameTime supports the use of Boolector with any of its recommended backend SAT solvers: Lingeling, MiniSat, or PicoSAT.

  • Z3: Add the path for the directory that contains the Z3 Python interface (z3.pyc) to the PATH system variable. This interface is usually located in the bin directory of the downloaded Z3 package.

In step 1, you installed the GNU Linear Programming Kit (glpk), which provides an ILP solver. However, using the pulp Python package, GameTime can also support the following ILP solvers (if installed): CBC mixed ILP solver, IBM ILOG CPLEX Optimizer, Gurobi Optimizer, and FICO Xpress Optimizer.

Step 3 (optional): Configuration of Simulator

This step is completely optional. You only need to follow this step if you do not already have a platform on which to run the generated test cases and to collect measurements, and if you would like to obtain your own measurements. In the tutorials, we have already provided these measurements for the test cases obtained for different demonstration files. Click here to show this step.

GameTime currently supports one simulator:

  1. PTARM simulator: This is a simulator for a precision-timed ARM architecture, developed by a collaborative effort lead by Prof. Edward A. Lee at University of California, Berkeley and Prof. Stephen A. Edwards at Columbia University.

    To install the PTARM simulator in Cygwin, follow the process described here, but with the following editions:

    1. If you are unable to access the website where the binaries for the GNU-ARM toolchain are located (http://gnuarm.com/files.html), you may be able to access an archived version of the website, such as the one located here.

    2. After the GNU-ARM toolchain has been installed as part of "Requirements", copy the DLL file cygwin1.dll from the root directory of Cygwin to the bin directory located within the root directory of the GNU-ARM toolchain.

    3. After the GNU-ARM toolchain has been installed as part of "Requirements", add the path to the directory libexec/gcc/arm-elf/4.1.1 to the PATH system variable. (To learn how to do this, refer to the appendix.)

    4. The simulator source code needs to be modified slightly. Before the step labeled "Compiling PTARM", navigate to the root directory of the simulator source code and run the following command in Cygwin to apply a patch to the source code:

      patch -d src/cpu < <GAMETIME_DIR>/ext/ptarm-sim.diff

      where GAMETIME_DIR is the path for the root directory of the GameTime source code.

    5. Once the simulator has been installed, add the path for the simulator executable (pret.exe) to the PATH system variable. (To learn how to do this, refer to the appendix.) The executable should be present in the bin directory located within the root directory of the simulator source code.

Step 4: Configuration of Cygwin, GameTime and Python

  1. Add the path for the directory that contains the Python interpreter, installed in the previous step, to the PATH system variable. (To learn how to do this, refer to the appendix.)

  2. Cygwin must be launched within the Microsoft Phoenix Command Prompt: right-click on Phoenix SDK Command Prompt - Debug - x86 under Microsoft Phoenix SDK June 2008 in the Start menu, and select Run as administrator.

  3. To launch Cygwin, enter the following command at the prompt: <CYGWIN_DIR>\cygwin.bat, where CYGWIN_DIR is the absolute path for the root directory of Cygwin, usually located at C:\cygwin.

  4. Navigate to the GameTime directory and run the following command at the prompt: ./configure && make install

    This command will configure different files within GameTime. It will then install the Python setuptools module, which will be used to install the following PyPI packages: networkx, numpy, ply, pulp, pyparsing, and pyside. Finally, GameTime itself will be installed as a Python module.

Step 5: Test of Installation

To test your installation, navigate to the GameTime directory in the Phoenix window running Cygwin. From within the directory, run the command: ./verify-installation

This should conduct a GameTime analysis on exemplar code that performs modular exponentiation, available in the directory demo/modexp_unrolled. GameTime should run completely without producing errors.

The command assumes default values for the solvers that GameTime uses in its verification of the installation: The default SMT solver is Z3 and the default ILP solver is the solver that is included with the pulp Python package.

To specify a different ILP solver, use the -i (or --ilp-solver) command-line switch, followed by the name of the ILP solver. The names supported are the same as those supported by the <ilp-solver> tag in a project configuration file, as enumerated here.

To specify a different SMT solver, use the -s (or --smt-solver) command-line switch, followed by the name of the SMT solver. The names supported are the same as those supported by the <smt-solver> tag in a project configuration file, as enumerated here.

So, for example, if the ILP solver available is GLPK and the SMT solver available is Boolector, the corresponding verification command would be ./verify-installation -i glpk -s boolector

If you have successfully installed GameTime, try out the tutorials.

Appendix: Modification of the PATH System Variable

To add a path to the PATH system variable, add this line to the end of the .bashrc file for Cygwin, usually located in the home subdirectory of the Cygwin directory:

PATH=<NEW_PATH>:$PATH

where NEW_PATH is the Unix form of the absolute path that needs to be added. So, for example, if the directory of the Python interpreter is located at C:\Python27, and this directory needs to be added to the PATH system variable, NEW_PATH will be /cygdrive/c/Python27. The command cygpath -u can be used to determine NEW_PATH.