Update installation instructions

Signed-off-by: Diogo Behrens <diogo.behrens@huawei.com>

Makefile

@@ -1,13 +1,15 @@
 PREFIX     ?= /usr/local
 BUILD       = build
-GENERATED   = $(shell find -name *_string.go)
 TAG        ?= $(shell git describe --always --tags --dirty)
 DOCKER_TAG ?= latest
-USE_DOCKER ?= false
+USE_DOCKER ?= true
 LDXFLAGS    = -X main.version=$(TAG) \
               -X vsync/tools.useDocker=$(USE_DOCKER) \
               -X vsync/tools.dockerTag=$(DOCKER_TAG)
 LDFLAGS     = -ldflags='-extldflags=-static $(LDXFLAGS)'
+
+SOURCES     = $(shell find -name '*.go' -not -name '*_string.go')
+GENERATED   = $(shell find -name *_string.go)
 ################################################################################
 # user goals
 ################################################################################
@@ -25,9 +27,9 @@ help:
 
 all: build
 
-build: generate build/vsyncer
+build: generate $(BUILD)/vsyncer
 
-install: build
+install: $(BUILD)/vsyncer
 	install $(BUILD)/vsyncer $(PREFIX)/bin/
 clean:
 	rm -rf $(BUILD) $(GENERATED)
@@ -38,9 +40,9 @@ clean:
 .PHONY: build-dir generate
 
 build-dir:
-	mkdir -p $(BUILD)
+	@mkdir -p $(BUILD)
 
-$(BUILD)/vsyncer: build-dir $(shell find -name '*.go')
+$(BUILD)/vsyncer: build-dir $(SOURCES)
 	env CGO_ENABLED=0 go build $(LDFLAGS) -o $@ ./cmd/vsyncer
 
 ################################################################################

README.md

@@ -1,7 +1,7 @@
-# vsyncer --- verifying and optimizing concurrent code on WMM
+# vsyncer -- verifying and optimizing concurrent code on WMMs
 
 `vsyncer` is a toolkit to verify and optimize concurrent C/C++ programs on Weak
-Memory Models (WMM).  The correctness of the target program is verified with
+Memory Models (WMMs).  The correctness of the target program is verified with
 state-of-the-art model checkers [Dartagnan][] and [GenMC][].  Optimization
 of the memory ordering of atomic operations is achieved by speculative
 verification of LLVM-IR mutations of the target program with feedback from
@@ -15,30 +15,58 @@ data structures and synchronization primitives verified and optimized with
 
 ## Installation
 
-### Runtime dependencies
+### Precompiled and Docker
 
-To run vsyncer you'll need the following tools:
+The simplest approach to run `vsyncer` is by using the prebuilt binary and
+a Docker container with its dependencies.  In more detail:
 
-- clang and llvm >= v10
-- Dartagnan >= v4.0.0 (alternative)
-- GenMC >= v0.8 (alternative)
+- download the binary of the current release,
+- change the name of the file to `vsyncer`, and then
+- either install the file in your `PATH` with `install vsyncer /some/path/bin`,
+- or set the file permissions with `chmod 755 vsyncer`.
+
+After that run `vsyncer docker --pull` to fetch the docker container with
+the dependencies (GenMC, Dartagnan, clang, etc).
+
+We assume that your user has rights to run docker, ie, either with rootless
+Docker or having your user in the `docker` group.  Please read the Docker
+[postinstall instructions][] further instructions.
+
+> Note: we have not yet tested `vsyncer` in macOS or Windows.
+
+### Building from source
+
+You will need Golang >= 1.18. Clone this repository and then run
+
+    make install PREFIX=/path/to/bin
 
-You can have them installed on your system or use docker containers.
+By default, `vsyncer` uses the runtime dependencies from the Docker image
+`ghcr.io/open-s4c/vsyncer` with tag `latest`. In contrast, precompiled
+releases use the fixed tag of the release.
 
-### Build from source
+To select a specific Docker image tag set `DOCKER_TAG` when installing
+`vsyncer`:
 
-Beyond the runtime dependencies, you'll need Golang >= v1.18 to build
-`vsyncer` from source.
+    make install PREFIX=/path/to/bin DOCKER_TAG=v2.0.0
 
-Assuming `go` and `make` are on your path, simply run
+### Disabling Docker
 
-    make
-    cp build/vsyncer /directory/on/your/path
+To run `vsyncer` without Docker, you'll need the following tools:
 
-If you do not have make installed, simply build it with
+- clang and llvm >= v14
+- Dartagnan >= v4.0.0 (alternative)
+- GenMC >= v0.9 (alternative)
+
+When installing `vsyncer` from source, set `USE_DOCKER=false` so that
+the binary does not try to use Docker but instead call the tools as
+normal programs in the host:
 
-    go build -o vsyncer ./cmd/vsyncer
-    cp vsyncer /directory/on/your/path
+    make install PREFIX=/path/to/bin USE_DOCKER=false
+
+We assume these tools are in `PATH`, but you can ajust that with the
+environment variables `DARTAGNAN_JAVA_CMD`, `GENMC_CMD` and `CLANG_CMD`.
+See `vsyncer -h` for more information about the configuration via
+environment variables.
 
 ## Overview
 
@@ -82,21 +110,17 @@ as a **bitsequence**  such as `0b001101` or `0x1a40`.
 *A*, *X*, and *F* assignments take bitsequences in which each **pair** of bits represent the memory ordering of a specific atomic operation.
 The memory may be relaxed (`0b00`),  release (`0b01`), acquire (`0b10`), or sequentially consistent (`0b11`).
 
-### Quick start
-
-#### Installation
+## Quick start
 
-    go build -o /dir/in/path/vsyncer ./cmd/vsyncer
-
-#### Retrieving information from program
+### Retrieving information from program
 
     vsyncer info example/ttaslock.c
 
-#### Checking whether program is correct
+### Checking whether program is correct
 
     vsyncer check example/ttaslock.c
 
-#### Mutating program with a memory ordering assignment:
+### Mutating program with a memory ordering assignment:
 
     vsyncer mutate -o ttaslock.ll example/ttaslock.c -A 0x123
     vsyncer info ttaslock.ll
@@ -105,7 +129,7 @@ To make all memory orderings be sequential consistent, you have to set all
 the bits of the bitsequences. Since this is used quite often, `vsyncer`
 accepts -1 as a shortcut for a bitsequence with all bits set.
 
-#### Checking mutation
+### Checking mutation
 
     vsyncer check ttaslock.ll
 
@@ -119,7 +143,6 @@ ordering first.
 
     vsyncer optimize -A -1 example/ttaslock.c
 
-
 ## Limitations
 
 ### Function pointers
@@ -168,7 +191,6 @@ The dependencies have the following licenses:
 
 Use [go-licenses](https://github.com/google/go-licenses) to review the licenses.
 
-
 ## Development information and contact
 
 Directory structure is as follows:
@@ -188,3 +210,4 @@ This project is under the support of [OpenHarmony Concurrency & Coordination TSG
 [Dartagnan]: https://github.com/hernanponcedeleon/Dat3M
 [GenMC]: https://github.com/MPI-SWS/genmc
 [libvsync]:  https://github.com/open-s4c/libvsync
+[postinstall instructions]: https://docs.docker.com/engine/install/linux-postinstall