(* ========================================================================= *) (* *) (* Formal Analysis of Hadoop Schedulers *) (* *) (* (c) Copyright, Mbarka Soualhia, 2017 *) (* Hardware Verification Group, *) (* Concordia University *) (* *) (* Contact: *) (* *) (* Last update: Dec 2017 *) (* *) (* ========================================================================= *) DESCRIPTION: See each file individually for a description of their contents in their header. We provide the CSP code to analyze the schedulability, fairness, and resources deadlock in Hadoop schedulers. We provide the description of each property in a seperate folder, where we include the description of the three schedulers: FIFO, Fair and Capacity INSTALLATION: To install the latest version of the PAT modecl checker Please follow the steps provided in: http://sav.sutd.edu.sg/PAT/?page_id=2587 How to use: 1. Launch PAT model checker 2. Load one CSP file from the provided ones 3. Compile it using the tool 4. Verify the given properties (the user may change teh given properties) For more information about PAT and CSP please visit: http://sav.sutd.edu.sg/PAT/?page_id=2611