Fix memory usage issue in SHA512-384-SELECTCHECK (#84)

SAW/proof/AES/AES-GCM-check-entrypoint.go

@@ -38,7 +38,7 @@ func main() {
 		wg.Add(1)
 		saw_template := "verify-AES-GCM-selectcheck-template.txt"
 		placeholder_name := "TARGET_LEN_PLACEHOLDER"
-		go utility.CreateAndRunSawScript(saw_template, placeholder_name, i, &wg)
+		go utility.CreateAndRunSawScript(saw_template, []string{}, placeholder_name, i, &wg)
 		utility.Wait(&process_count, num_parallel_process, &wg)
 	}
 

SAW/proof/SHA512/SHA512-384-check-entrypoint.go

@@ -8,11 +8,13 @@ package main
 import (
 	utility "aws-lc-verification/proof/common"
 	"log"
+	"math"
 	"os"
 	"sync"
 )
 
-const sha_process_limit int = 15
+const memory_used_per_test uint64 = 30e9
+const max_heap_size string = "-M30G"
 
 func main() {
 	log.Printf("Started SHA512-384 check.")
@@ -24,19 +26,24 @@ func main() {
 	}
 
 	// When 'SHA512_384_SELECTCHECK' is defined, formal verification is executed with all `len` given a 'num'.
-	// Due to memory usage (each select_check takes 8GB memory) and limit of container size (largest one has 145GB memory),
+	// Due to memory usage (each select_check takes 36-48GB memory) and limit of container size (largest one has 145GB memory),
 	// not all nums are used to run formal verification. Only below nums are selected.
 	target_nums := []int{0, 1, 2, 3, 5, 8, 13, 21, 34, 55, 89, 127}
 
 	// Generate saw scripts based on above verification template and target num ranges.
 	var wg sync.WaitGroup
 	process_count := 0
+
+	total_memory := utility.SystemMemory()
+	num_parallel_process := int(math.Floor((float64(total_memory) / float64(memory_used_per_test))))
 	for _, num := range target_nums {
 		wg.Add(1)
 		saw_template := "verify-SHA512-384-selectcheck-template.txt"
 		placeholder_name := "TARGET_NUM_PLACEHOLDER"
-		go utility.CreateAndRunSawScript(saw_template, placeholder_name, num, &wg)
-		utility.Wait(&process_count, sha_process_limit, &wg)
+		// Haskell runtime control, maximum heap size 30G
+		// https://downloads.haskell.org/~ghc/5.04.2/docs/html/users_guide/runtime-control.html
+		go utility.CreateAndRunSawScript(saw_template, []string{"+RTS", max_heap_size, "-RTS"}, placeholder_name, num, &wg)
+		utility.Wait(&process_count, num_parallel_process, &wg)
 	}
 
 	wg.Wait()

SAW/proof/common/utility.go

@@ -42,7 +42,7 @@ func ParseSelectCheckRange(env_var_name string, default_val int) int {
 }
 
 // A function to create a saw script, replace `placeholder_key` with value, and then execute the script.
-func CreateAndRunSawScript(path_to_template string, placeholder_key string, value int, wg *sync.WaitGroup) {
+func CreateAndRunSawScript(path_to_template string, saw_params []string,  placeholder_key string, value int, wg *sync.WaitGroup) {
 	log.Printf("Start creating saw script for target value %s based on template %s.", value, path_to_template)
 	// Create a new saw script.
 	file_name := fmt.Sprint(value, ".saw")
@@ -59,13 +59,14 @@ func CreateAndRunSawScript(path_to_template string, placeholder_key string, valu
 	defer os.Remove(file_name)
 	// Run saw script.
 	defer wg.Done()
-	RunSelectCheckScript(file_name, path_to_template)
+	RunSelectCheckScript(file_name, saw_params, path_to_template)
 }
 
 // A function to run saw script.
-func RunSelectCheckScript(path_to_saw_file string, path_to_template string) {
+func RunSelectCheckScript(path_to_saw_file string, saw_params []string, path_to_template string) {
 	log.Printf("Running saw script %s. Related template: %s.", path_to_saw_file, path_to_template)
-	cmd := exec.Command("saw", path_to_saw_file)
+	saw_command := append(saw_params, path_to_saw_file)
+	cmd := exec.Command("saw", saw_command...)
 	cmd.Stdout = os.Stdout
 	cmd.Stderr = os.Stderr
 	err := cmd.Run()

SAW/scripts/install.sh

@@ -7,7 +7,7 @@ set -ex
 
 Z3_URL='https://github.com/Z3Prover/z3/releases/download/z3-4.8.8/z3-4.8.8-x64-ubuntu-16.04.zip'
 YICES_URL='https://yices.csl.sri.com/releases/2.6.2/yices-2.6.2-x86_64-pc-linux-gnu-static-gmp.tar.gz'
-SAW_URL='https://saw-builds.s3.us-west-2.amazonaws.com/saw-0.9.0.99-Linux-x86_64.tar.gz'
+SAW_URL='https://saw-builds.s3.us-west-2.amazonaws.com/saw-0.9.0.99-2023-01-20-Linux-x86_64.tar.gz'
 
 mkdir -p /bin /deps