Commit ec0f2d13 authored by Etienne Renault's avatar Etienne Renault

go2pins: enable multithreading for backends

* Makefile,
benchs/run-benchmark.sh,
boilerplate/main.go: Here.
parent 2eaa308e
Pipeline #24570 passed with stage
in 2 minutes and 5 seconds
......@@ -24,7 +24,7 @@ all:
"Consider \"make release\" for a more efficient version "
release:
@go build -ldflags "-s -w" && go build -o ltlrec ltl/desugar/main.go
@go build -ldflags "-s -w" && go build -o ltlrec ltl/desugar/main.go
build-image: Dockerfile
docker build --no-cache -t registry.lrde.epita.fr/go2pins-debian .
......@@ -39,7 +39,7 @@ check: go2pins
@cd tests && ./run.sh
benchmark:
@make clean release && cd benchs && ./run-benchmark.sh
@make clean release && cd benchs && ./run-benchmark.sh $(nbthreads)
clean:
go clean
......
......@@ -70,10 +70,16 @@ FILES="RERS/2016-Problem10-reach.go \
RERS/2019-Problem14-reach.go \
RERS/2019-Problem15-reach.go "
OUTPUT=benchs.csv
OUTPUT_BB=benchs-bb.csv
OUTPUT_REACH=benchs-reach.csv
OUTPUT_LTL=benchs-ltl.csv
NBTHREADS=1
if [ $# -eq 1 ]; then
NBTHREADS=$1
fi
OUTPUT="benchs-$NBTHREADS.csv"
OUTPUT_BB="benchs-bb-$NBTHREADS.csv"
OUTPUT_REACH="benchs-reach-$NBTHREADS.csv"
OUTPUT_LTL="benchs-ltl-$NBTHREADS.csv"
echo "##################################"
......
......@@ -32,6 +32,7 @@ import (
"os/exec"
"path/filepath"
"regexp"
"strconv"
"strings"
"unsafe"
)
......@@ -376,6 +377,7 @@ var (
kripke_ss = flag.Bool("kripke-size", false, "The size of the state space (only spot backend)")
list_var = flag.Bool("list-variables", false, "Display the list of variable names.")
ltl = flag.String("ltl", "", "The LTL formulae to check")
nb_threads = flag.Int("nb-threads", 1, "The number of threads to use")
)
func init() {
......@@ -450,15 +452,28 @@ func main() {
if *ltl != "" {
var mcCmd *exec.Cmd
if *backend == "ltsmin" {
mcCmd = exec.Command(ltsmin_path(), "--threads", "1",
mcCmd = exec.Command(ltsmin_path(),
"--threads", strconv.Itoa(*nb_threads),
"--ltl", *ltl, maindve2C)
} else if *backend == "spot" || *backend == "" {
if !spot_dev_version() {
if *nb_threads != 1 {
panic ("This version of spot does not support multithreading")
}
mcCmd = exec.Command(spot_path(), maindve2C, "!"+*ltl)
} else {
mcCmd = exec.Command(spot_path(), "-e",
"--model", maindve2C,
"--formula", "!"+*ltl)
// Use BDD based algorithms
if *nb_threads == 1 {
mcCmd = exec.Command(spot_path(), "-e",
"--model", maindve2C,
"--formula", "!"+*ltl)
} else { // Use parallel algorithms
mcCmd = exec.Command(spot_path(), "-e",
"--model", maindve2C,
"--formula", "!"+*ltl,
"--parallel", strconv.Itoa(*nb_threads))
}
}
} else {
panic("backend '" + *backend + "' unknown!")
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment