diff --git a/org.lamport.tla.toolbox.jclouds/src/org/lamport/tla/toolbox/jcloud/AzureCloudTLCInstanceParameters.java b/org.lamport.tla.toolbox.jclouds/src/org/lamport/tla/toolbox/jcloud/AzureCloudTLCInstanceParameters.java index 87fc184c8546a05f9475410ae6ac0e85297d162e..5bc266f4cc5b0202d1f6283486303c208ca09ef3 100644 --- a/org.lamport.tla.toolbox.jclouds/src/org/lamport/tla/toolbox/jcloud/AzureCloudTLCInstanceParameters.java +++ b/org.lamport.tla.toolbox.jclouds/src/org/lamport/tla/toolbox/jcloud/AzureCloudTLCInstanceParameters.java @@ -196,4 +196,47 @@ public class AzureCloudTLCInstanceParameters extends CloudTLCInstanceParameters // (similar to EC2CloudTLCInstanceParameters#getHostnameSetup. return "hostname \"$(hostname).cloudapp.net\" && echo \"$(curl -s ifconfig.co) $(hostname)\" >> /etc/hosts"; } + + /* (non-Javadoc) + * @see org.lamport.tla.toolbox.jcloud.CloudTLCInstanceParameters#getCleanup() + */ + @Override + public String getCloudAPIShutdown() { + final String servicePrincipal = System.getenv("AZURE_COMPUTE_SERVICE_PRINCIPAL"); + final String password = System.getenv("AZURE_COMPUTE_SERVICE_PRINCIPAL_PASSWORD"); + final String tenant = System.getenv("AZURE_COMPUTE_SERVICE_PRINCIPAL_TENANT"); + if (servicePrincipal == null || password == null || tenant == null) { + // Missing credentials. + return super.getCloudAPIShutdown(); + } + // What we try to accomplish is to purge the complete Azure Resource Group (a RG + // combines all Azure resources associated with the VM (storage, networking, + // ips, ...). + // The way we do it, is to use the azure CLI to deploy the template in + // /tmp/rg.json created by the printf statement under the same resource group + // identify we wish to purge. The trick is, that the template defines no + // resources whatsoever. This effectively purges the old resources in the + // resource group. Idea taken from + // http://www.codeisahighway.com/effective-ways-to-delete-resources-in-a-resource-group-on-azure/ + // bash/screen/ssh apparently fiddle with quotes and which is why the json is base64 encoded + // and decoded on the instance: + // { "$schema": "https://schema.management.azure.com/schemas/2015-01-01/deploymentTemplate.json#", "contentVersion": "1.0.0.0", "parameters": {}, "variables": {}, "resources": [], "outputs": {} } | base64 + // + // Unfortunately, the azure CLI needs credentials to talk to the Azure API. For + // that, one manually creates a service principal once as described in + // https://docs.microsoft.com/en-us/cli/azure/create-an-azure-service-principal-azure-cli?view=azure-cli-latest + // and uses it to log into Azure as described in + // https://docs.microsoft.com/en-us/cli/azure/authenticate-azure-cli?view=azure-cli-latest. + // Using AZURE_COMPUTE_CREDENTIALS and AZURE_COMPUTE_IDENTITY to login with azure CLI + // would trigger a two-factor auth for Microsoft FTEs. Not something we want. + // + // An alternative might be to use an auth.properties file, but this doesn't seem + // supported by azure CLI yet. Read "File based authentication" at + // https://docs.microsoft.com/en-us/java/azure/java-sdk-azure-authenticate#mgmt-file + return "echo eyAiJHNjaGVtYSI6ICJodHRwczovL3NjaGVtYS5tYW5hZ2VtZW50LmF6dXJlLmNvbS9zY2hlbWFzLzIwMTUtMDEtMDEvZGVwbG95bWVudFRlbXBsYXRlLmpzb24jIiwgImNvbnRlbnRWZXJzaW9uIjogIjEuMC4wLjAiLCAicGFyYW1ldGVycyI6IHt9LCAidmFyaWFibGVzIjoge30sICJyZXNvdXJjZXMiOiBbXSwgIm91dHB1dHMiOiB7fSB9Cg== | base64 -d > /tmp/rg.json" + + " && " + "az login --service-principal -u \"" + servicePrincipal + "\" -p " + password + " --tenant " + // $(hostname -s) only works iff hostname is correctly setup with getHostnameSetup() above. + + tenant + " && " + "az group deployment create --resource-group $(hostname -s)" + + " --template-file /tmp/rg.json --mode Complete"; + } } diff --git a/org.lamport.tla.toolbox.jclouds/src/org/lamport/tla/toolbox/jcloud/CloudDistributedTLCJob.java b/org.lamport.tla.toolbox.jclouds/src/org/lamport/tla/toolbox/jcloud/CloudDistributedTLCJob.java index fd8c78d619c9230900f69e654904881cc2823edb..b66caf888dff68e00142d56b4212d75fdb085688 100644 --- a/org.lamport.tla.toolbox.jclouds/src/org/lamport/tla/toolbox/jcloud/CloudDistributedTLCJob.java +++ b/org.lamport.tla.toolbox.jclouds/src/org/lamport/tla/toolbox/jcloud/CloudDistributedTLCJob.java @@ -348,6 +348,12 @@ public class CloudDistributedTLCJob extends Job { + "-jar /tmp/tla2tools.jar " + params.getTLCParameters() + " " + "&& " + // Run any cloud specific cleanup tasks. + // When CloudDistributedTLCJob runs in synchronous CLI mode (isCLI), it will destroy + // the VMs (nodes) via the jclouds API. No need to deallocate nodes + // via special logic. + + (isCLI ? "/bin/true" : params.getCloudAPIShutdown()) + + " && " // Let the machine power down immediately after // finishing model checking to cut costs. However, // do not shut down (hence "&&") when TLC finished @@ -461,6 +467,9 @@ public class CloudDistributedTLCJob extends Job { // to a NoRouteToHostException when the master // shut down caused by a violation among the // init states. + // Run any cloud specific cleanup tasks. + + params.getCloudAPIShutdown() + + " && " + "sudo shutdown -h now" + "\""), new TemplateOptions().runAsRoot(false).wrapInInitScript( diff --git a/org.lamport.tla.toolbox.jclouds/src/org/lamport/tla/toolbox/jcloud/CloudTLCInstanceParameters.java b/org.lamport.tla.toolbox.jclouds/src/org/lamport/tla/toolbox/jcloud/CloudTLCInstanceParameters.java index 4fb6fba0d388ad9c9b6f9cfffa1a9e90d4fef0ab..7cbba7e80648da18bde2b77319612d5c7b21ba2f 100644 --- a/org.lamport.tla.toolbox.jclouds/src/org/lamport/tla/toolbox/jcloud/CloudTLCInstanceParameters.java +++ b/org.lamport.tla.toolbox.jclouds/src/org/lamport/tla/toolbox/jcloud/CloudTLCInstanceParameters.java @@ -140,6 +140,10 @@ public abstract class CloudTLCInstanceParameters { return "/bin/true"; // no-op, because concat with && ... && in CDTJ. } + public String getCloudAPIShutdown() { + return "/bin/true"; // no-op, because concat with && ... && in CDTJ. + } + public String getExtraRepositories() { return "/bin/true"; // no-op, because concat with && ... && in CDTJ. }