HTTPS SSH
#sudiptac: MESS is a memory-performance checker for multi-core systems

#Current limitation: MESS currently checks memory for programs that 
#execute on disjoint memory spaces. In other words, MESS checks 
#performance for embarassingly parallel software.

#check our SPIN 2015 paper or the extended version for more information:
#(http://sudiptac.bitbucket.org/papers/mess_spin2015.pdf)
#(http://sudiptac.bitbucket.org/papers/mess-extended.pdf)

**************************
README section for MESS:
**************************
MESS is developed on constraint solver Z3 (using QF_LIA theory) and 
simplescalar simulator.

This is a compositional performance debugging framework based on Z3 
constraint solver. To push the content use the following hg command:

hg push https://sudiptac@bitbucket.org/sudiptac/mess

Let us assume "Z3_root" captures the root directory for Z3.

MESS constraint system is available here:
 
	Z3_root/project/Timing_Compositional

Modified simulator (to generate shared-cache access traces) 
is available here:

	Z3_root/project/CMP_SIM/simplesim-3.0

Compiling MESS:

	- Goto Z3_root/build
	- type "make project"

	This will create an executable "timing" in Z3_root/build

Try MESS on a small example:

	- Goto Z3_root/build
	- Execute "./timing lruc localinput/small/shared_cache_lru.dat"

	This will create the constraint file (in smt2 format) 
	"shared_cache_lru.dat.smt2" at directory localinput/small. 
	This will also create other files for the approximation scheme 
	to run.

MESS running format:

	Once you have successfully installed Z3 and compiled MESS, you can 
	try MESS on several examples. Following is the execution format of 
	MESS:

	./timing {replacement policy} {trace file} [threshold] [cache size]

	Where different arguments has the following interpretation:

	{replacement policy:} Cache replacement policy. Currently, least 
	recently used (LRU) and first-in-first-out (FIFO) policies are 
	implemented. Type "lruc" to include caches with LRU policy and type 
	"fifoc" to include caches with FIFO policy.

	{trace file:} This is the file where we record the shared-cache 
	accesses from each core in isolation. Let us assume that we have 
	a dual-core system, then "<filename>.0" and "<filename>.1" provide 
	the trace file for core 0 and core 1, respectively. These files 
	have been generated by the modified simplescalar simulator. Look 
	at the "localinput" and "localinput_FIFO" directories for sample 
	trace files.

	{threshold:} We check temporal constraints of the form "Delta <= T". 
	Threshold provides the value of T. Default value is set to 1200 CPU 
	cycles, which means 12 shared-cache misses.

	{cache size:} Provide the size of caches in the following format: 
			number_of_sets:line_size(in bytes):associativity
	For instance, 4-way, 2 KB cache, with 32 bytes line size, can be 
	provided as "16:32:4".

Example scripts:

	There has been scripts provided to run different examples. Please 
	look at the following scripts:

	rconfig_timing/exp_threshold/run_timing 
	and 
	rconfig_timing/exp_threshold/run_timing_one
	
	rconfig_timing/exp_threshold_FIFO/run_timing 
	and 
	rconfig_timing/exp_threshold_FIFO/run_timing_one

For running the MESS approximation scheme:
	This requires a tool "symba" to be installed. Please follow 
	the instructions in https://bitbucket.org/arieg/symba to install 
	symba. Our approximation scheme internally invokes symba inside 
	a script. Therefore, the approximation will not run without symba 
	being installed in your system.

	Our approximation scheme produces constraint system for each 
	cache set. These constraints can be solved independently and in 
	parallel. We do not have a parallel implementation now, we 
	currently sequentialize the handling of set-based constraint 
	system. 

	Run "./timing lruc localinput/small/shared_cache_lru.dat"

	In localinput/small, you will find files of the following format:

	localinput/small/shared_cache_lru.dat.smt2.<set>

	where <set> captures the constraint system for cache set number 
	<set>.

	"symba" is invoked to optimize this set-based constraint system 
	as follows:

	symba -b=localinput/small/shared_cache_lru.dat.smt2.<set> -opti-z3=true 

	For example scripts, please follow:

	rconfig_timing/exp_bound/run_timing
	and 
	rconfig_timing/exp_bound/run_timing_one

For generating trace file:

	Trace files are generated by the modified simplescalar simulator.
	A general README file to run the simulator has been provided here:

	Z3_root/project/CMP_SIM/simplesim-3.0/README

	Check the following scripts to generate trace files:

	Z3_root/project/CMP_SIM/simplesim-3.0/run_cache
	Z3_root/project/CMP_SIM/simplesim-3.0/run_cache_FIFO
	
	NOTE: Be careful in running the scripts, as it may delete some 
	old contents.

To rerun the existing experiments (NOTE: experiments may run for long):

	Experiments for LRU caches, do the following:
	
	cd Z3_root/project/CMP_SIM/simplesim-3.0
	./run_cache #produces trace files at Z3_root/build/localinput
	cd Z3_root/build
	./rconfig_timing/exp_threshold/run_timing
	
	Experiments for FIFO caches, do the following:
	
	cd Z3_root/project/CMP_SIM/simplesim-3.0
	./run_cache_FIFO #produces trace files at Z3_root/build/localinput_FIFO
	cd Z3_root/build
	./rconfig_timing/exp_threshold_FIFO/run_timing

	Experiments for approximation (LRU), do the following:

	cd Z3_root/build
	./rconfig_timing/exp_bound/run_timing
	
	Experiments for approximation (FIFO), do the following:

	cd Z3_root/build
	./rconfig_timing/exp_bound_FIFO/run_timing

	Sensitivity Experiments for LRU caches, do the following:
	
	cd Z3_root/project/CMP_SIM/simplesim-3.0
	./run_sens #produces trace files at Z3_root/build/localinput_sens
	cd Z3_root/build
	./rconfig_timing/exp_sens/run_timing
	
	Sensitivity Experiments for LRU caches, do the following:
	
	cd Z3_root/project/CMP_SIM/simplesim-3.0
	./run_sens_FIFO #produces trace files at Z3_root/build/localinput_sens_FIFO
	cd Z3_root/build
	./rconfig_timing/exp_sens_FIFO/run_timing

That's all folks. If you face difficulty in installing or running the tools, 
feel free to contact me (sudipta.chattopadhyay@liu.se).
	
=======================================================================================

************************
README section for Z3:
************************

Z3 is a theorem prover from Microsoft Research.
Z3 is licensed under MSR-LA (Microsoft Research License Agreement). 
See http://z3.codeplex.com/license for more information about this license.
Z3 can be built using Visual Studio Command Prompt and make/g++.

1) Building Z3 on Windows using Visual Studio Command Prompt
   
   python scripts/mk_make.py
   cd build
   nmake

2) Building Z3 using make/g++ and Python
Execute:

   autconf
   ./configure
   python scripts/mk_make.py
   cd build
   make
   sudo make install

It will install z3 executable at /usr/bin, libraries at /usr/lib, and include files at /usr/include.
You can change the installation p

Use the following commands to install in a different prefix (e.g., /home/leo).

  autoconf
  ./configure --prefix=/home/leo
  python scripts/mk_make.py
  cd build
  make
  sudo make install

To uninstall Z3, use

  sudo make uninstall

3) Building Z3 using clang++ on Linux/OSX
Remark: clang does not support OpenMP yet.   

   autoconf
   ./configure CXX=clang++
   python scripts/mk_make.py
   cd build
   make