Using Amazon EC2 virtual machines as computational backend - iteloo/formality-tools GitHub Wiki

Even for relatively small dgla's, the test for formality often involve extremely large linear systems that have to be computed and then solved. Here we describe how to leverage the computational power of Amazon's Elastic Compute Cloud (EC2) service to achieve this.

Launching an EC2 instance

You can get started here. The pricing depends on how much computation resources you require. For my problems, I used the cr1.8xlarge cluster instance.

Setting up SSH

To make making SSH connections more convenient, edit your ~/.ssh/config on your local machine (or create one if it doesn't already exist). Add the following lines:

host aws
hostname <<public-ip-of-instance>>
user ec2-user
IdentityFile <<path-to-key>>

where <<path-to-key>> is where you store the .pem file created for you when the instance is launched. Finally, make sure that your instance does allow SSH connection (i.e. port 22 should be on the list of allowed ports in the security group, which you can edit on the EC2 online dashboard.)

Setting up Mathematica and MATLAB

Possible issue with size of root device

When my cr1.8xlarge instances were launched, the system only sees 6GB of free space instead of whatever I specify in the options when I launch the instance online. To resolve this, follow Resizing the root device on Amazon EC2.