Skip to content
This repository has been archived by the owner on Aug 26, 2022. It is now read-only.

Home

Jump to bottom
Priyan Vaithilingam edited this page Feb 26, 2018 · 10 revisions

PSharp Batch Testing

PSharp batch testing is an Addon for PSharp language.

Overview

PSharp batch tester uses Azure Batch Service to run multiple PSharp tests in parallel on the cloud and fetch the result. Using this tool you can run heavy testing in the cloud.

Running PSharp Batch Tests

To run Psharp batch test, you need an Azure subscription and an Azure batch service account. To learn more about creating an Azure batch service account, view the sub-heading Azure Batch Service. Once you have that, follow the steps below:

  1. Open the solution containing the PSharp project you need to test.

  2. Install the Microsoft.PSharp.BatchTesting nuget from here: Microsoft.PSharp.Nuget.

  3. Installing the Nuget will add two config files to the project.

    • PSharpBatch.config : Contains configuration for uploading necessary files, testing in the cloud and downloading the results.
    • PSharpBatchAuth.config : authentication credentials for Azure batch account and storage account.

    (For more details about configuration go to: Configuring Batch Test).

  4. Edit the configuration files to need and Open Nuget Package Manager Console.

  5. Run the command BatchTest in Nuget Package Manager Console to start the Batch Testing.

Command Line Arguments

  1. /config:<filename> : Path to PSharpBatch config file.
  2. /auth:<filename> : Path to PSharpBatchAuth config file.
  3. /monitor : If /psbatch flag is provided, monitor existing job. If not, run new job and monitor.
  4. /psbatch:<filename> : Cache file to help monitoring existing azure job.

Configuring Batch Test

Configuring PSharpBatch.config

Sample config file can be found here

PSharpBatch.config has the following parameters:

  • PoolId : Id of the virtual machine pool in Azure batch service. If it doesn't exists already, it will be created.
  • NumberOfNodesInPool : Number of VMs to be added in the pool, if it is created.
  • NodeOsFamily : The OS version of the VMs. Should contain .Net Framework 4.6 and above (OsFamily: >=5). For more details visit: Azure Guest OS Update Matix.
  • NodeMaxConcurrentTasks : Maximum number of concurrent tasks per node (default:1).
  • NodeVirtualMachineSize : Size of each virtual machine. For more details on virtual machine sizes visit: Virtual Machine Sizes
  • JobDefaultId : Prefix for the Job to be created for the given tests. This will be appended by time-stamp.
  • TaskDefaultId : Prefix for the tasks created under the Job. Will be appended by JobId and time-stamp.
  • BlobContainerSasExpiryHours (deprecated) : Exipry time in hours for the files uploaded to storage account. After this time period, the Batch service will not be able to use the files. -1 for no expiry.
  • PSharpBinariesFolderPath : Path to folder containing PSharp Binaries.
  • OutputFolderPath : Path to folder where the output should be downloaded.
  • TaskWaitHours : Waiting time in hours for the test to complete. Post this time, the unfinished tasks will be terminated.
  • DeleteJobAfterDone : (true/false) Whether to delete the Batch-service job after it is complete.
  • DeleteContainerAfterDone : (true/false) Whether to delete the storage account containers after the tests are complete.
  • DeletePoolAfterDone : (true/false) Whether to delete the Azure Pool after job is complete.
  • RunLocally : (true/false) If enabled, will run the test locally instead of the cloud.
  • Tests : The batch tester can run multiple tests consisting of many commands. Use the <Test> tag to add multiple tests.
    • Name(attribute)(optional) - Path to the binary to be tested (.dll/.exe).
    • ApplicationPath - Path to the binary to be tested (.dll/.exe).
    • Command : Tests commands to run in cloud. You can have multiple commands under a single <Test> tag.
      • CommandName(attribute) : A name to command to distinguish between different tasks.
      • Flags(attribute) : Flags / arguments for the test command. Requires iterations flag (/i) and parallel flag (/parallel).

Configuring PSharpBatch.Auth.config

Sample Auth config file can be found here

PSharpBatchAuth.config has the following parameters:

  • BatchAccountName : Name of the Azure Batch Service Account.
  • BatchAccountKey : Account Key for the Azure Batch Service Account.
  • BatchAccountUrl : URL of the Azure Batch Service Account.
  • StorageAccountName : Name of the Storage Account linked with the Azure Batch Service Account.
  • StorageAccountKey : Account Key (Primary/Secondary) of the above mentioned Storage Account.

Configuring Azure Batch Service

To configure Azure Batch service you need an active Azure subscription.

Creating a Batch Service Account

  1. Open the azure portal, and click New button.
  2. In the search bar search for Batch Service, and select the Batch Service option from the result.
  3. Click create and enter the required details. Also in this step create a new Storage Account and associate with the Batch Service before clicking create.
  4. After deployment is complete, you can go to the Batch account.
  5. The overview will give you the URL and the name of the account (Which you entered when creating the account).
  6. Go to the Keys tab and copy the Primary access key.
  7. You will need to Enter the account name, URL and the access key in PSharpBatchAuth.config.
  8. You can manually create the Pool from Azure Portal, or create using the PSharp Batch tester tool.
Clone this wiki locally