From 9de378e9b0489775a41dedea085e9d77ca52e256 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Lo=C3=AFc=20Hoguin?= Date: Thu, 18 Jun 2020 15:02:43 +0200 Subject: Add initial Concuerror integration https://concuerror.com/ --- CHANGELOG.asciidoc | 4 ++ build.config | 1 + doc/src/guide/book.asciidoc | 2 + doc/src/guide/concuerror.asciidoc | 77 +++++++++++++++++++++++++++++++++++++++ plugins/concuerror.mk | 67 ++++++++++++++++++++++++++++++++++ test/plugin_concuerror.mk | 39 ++++++++++++++++++++ 6 files changed, 190 insertions(+) create mode 100644 doc/src/guide/concuerror.asciidoc create mode 100644 plugins/concuerror.mk create mode 100644 test/plugin_concuerror.mk diff --git a/CHANGELOG.asciidoc b/CHANGELOG.asciidoc index cdffb29..f0ff0e2 100644 --- a/CHANGELOG.asciidoc +++ b/CHANGELOG.asciidoc @@ -19,3 +19,7 @@ `-lei` which is part of the Erlang/OTP Erl_Interface *application* but is built as a separate C library. The removal only applies to `-lerl_interface` itself. + +2020/06/18: Concuerror integration has been added. It is + currently minimal but usable. Experimentation + and feedback is welcome. diff --git a/build.config b/build.config index bcf2b9a..a0ab7a7 100644 --- a/build.config +++ b/build.config @@ -22,6 +22,7 @@ plugins/asciidoc plugins/bootstrap plugins/c_src plugins/ci +plugins/concuerror plugins/ct plugins/dialyzer plugins/edoc diff --git a/doc/src/guide/book.asciidoc b/doc/src/guide/book.asciidoc index fa31fe3..7c4ee68 100644 --- a/doc/src/guide/book.asciidoc +++ b/doc/src/guide/book.asciidoc @@ -64,6 +64,8 @@ include::ci.asciidoc[Continuous integration] include::dialyzer.asciidoc[Dialyzer] +include::concuerror.asciidoc[Concuerror] + include::xref.asciidoc[Xref] [[plugins]] diff --git a/doc/src/guide/concuerror.asciidoc b/doc/src/guide/concuerror.asciidoc new file mode 100644 index 0000000..160af74 --- /dev/null +++ b/doc/src/guide/concuerror.asciidoc @@ -0,0 +1,77 @@ +[[concuerror]] +== Concuerror + +https://concuerror.com/[Concuerror] is a stateless model +checking tool for Erlang programs. It can be used to detect +and debug concurrency errors, such as deadlocks and errors +due to race conditions. The key property of such errors is +that they only occur on few, specific schedulings of the +program. Moreover, unlike tools based on randomisation, +Concuerror can verify the absence of such errors, because +it tests the program systematically. + +Erlang.mk provides a wrapper around Concuerror. + +=== Configuration + +The `CONCUERROR_TESTS` variable must be defined in order to +use Concuerror. It lists the Concuerror test cases. There +is currently no way to detect test cases automatically. The +tests must be listed as `module:function` separated by +whitespace. For example: + +[source,make] +CONCUERROR_TESTS = ranch_concuerror:start_stop ranch_concuerror:info + +Concuerror will output some information directly on the +screen when run, but errors will only be written to a file. +This is because the error output can be very large. By +default Erlang.mk instructs Concuerror to save log files +in the 'logs/' directory (shared with Common Test). This +can be changed by setting `CONCUERROR_LOGS_DIR`: + +[source,make] +CONCUERROR_LOGS_DIR = $(CURDIR)/path/to/logs + +Concuerror options can be specified using the +`CONCUERROR_OPTS` variable: + +[source,make] +CONCUERROR_OPTS = -k + +Note that options may also be specified on a per-module +basis using the `-concuerror_options([]).` attribute. + +=== Writing tests + +Concuerror tests are a simple 0-arity function that must +be exported. For example: + +[source,erlang] +---- +-export([info/0]). + +info() → + %% Ensure we can call ranch:info/1 after starting a listener. + SupPid = do_start(), + {ok, _} = ranch:start_listener(?FUNCTION_NAME, + ranch_erlang_transport, #{ + num_acceptors ⇒ 1 + }, + echo_protocol, []), + #{} = ranch:info(?FUNCTION_NAME), + do_stop(SupPid). +---- + +Do not forget to add the function to `CONCUERROR_TESTS` +as well. + +=== Usage + +To run Concuerror: + +[source,bash] +$ make concuerror + +Erlang.mk will create an index of all the test logs in +the '$(CONCUERROR_LOGS_DIR)/concuerror.html' file. diff --git a/plugins/concuerror.mk b/plugins/concuerror.mk new file mode 100644 index 0000000..ef63add --- /dev/null +++ b/plugins/concuerror.mk @@ -0,0 +1,67 @@ +# Copyright (c) 2020, Loïc Hoguin +# This file is part of erlang.mk and subject to the terms of the ISC License. + +ifdef CONCUERROR_TESTS + +.PHONY: concuerror distclean-concuerror + +# Configuration + +CONCUERROR_LOGS_DIR ?= $(CURDIR)/logs +CONCUERROR_OPTS ?= + +# Core targets. + +check:: concuerror + +ifndef KEEP_LOGS +distclean:: distclean-concuerror +endif + +# Plugin-specific targets. + +$(ERLANG_MK_TMP)/Concuerror/bin/concuerror: | $(ERLANG_MK_TMP) + $(verbose) git clone https://github.com/parapluu/Concuerror $(ERLANG_MK_TMP)/Concuerror + $(verbose) make -C $(ERLANG_MK_TMP)/Concuerror + +$(CONCUERROR_LOGS_DIR): + $(verbose) mkdir -p $(CONCUERROR_LOGS_DIR) + +define concuerror_html_report + + + + +Concuerror HTML report + + +

Concuerror HTML report

+

Generated on $(concuerror_date)

+ + + +endef + +concuerror: $(addprefix concuerror-,$(subst :,-,$(CONCUERROR_TESTS))) + $(eval concuerror_date := $(shell date)) + $(eval concuerror_targets := $^) + $(verbose) $(call core_render,concuerror_html_report,$(CONCUERROR_LOGS_DIR)/concuerror.html) + +define concuerror_target +.PHONY: concuerror-$1-$2 + +concuerror-$1-$2: test-build | $(ERLANG_MK_TMP)/Concuerror/bin/concuerror $(CONCUERROR_LOGS_DIR) + $(ERLANG_MK_TMP)/Concuerror/bin/concuerror \ + --pa $(CURDIR)/ebin --pa $(TEST_DIR) \ + -o $(CONCUERROR_LOGS_DIR)/concuerror-$1-$2.txt \ + $$(CONCUERROR_OPTS) -m $1 -t $2 +endef + +$(foreach test,$(CONCUERROR_TESTS),$(eval $(call concuerror_target,$(firstword $(subst :, ,$(test))),$(lastword $(subst :, ,$(test)))))) + +distclean-concuerror: + $(gen_verbose) rm -rf $(CONCUERROR_LOGS_DIR) + +endif diff --git a/test/plugin_concuerror.mk b/test/plugin_concuerror.mk new file mode 100644 index 0000000..f1b9288 --- /dev/null +++ b/test/plugin_concuerror.mk @@ -0,0 +1,39 @@ +# Concuerror plugin. + +CONCUERROR_TARGETS = $(call list_targets,concuerror) + +.PHONY: concuerror $(CONCUERROR_TARGETS) + +concuerror: $(CONCUERROR_TARGETS) + +concuerror-app: init + + $i "Bootstrap a new OTP application named $(APP)" + $t mkdir $(APP)/ + $t cp ../erlang.mk $(APP)/ + $t $(MAKE) -C $(APP) -f erlang.mk bootstrap $v + + $i "Create a test module with a function that returns immediately" + $t mkdir $(APP)/test + $t printf "%s\n" \ + "-module(concuerror_success)." \ + "-export([test/0])." \ + "test() -> ok." > $(APP)/test/concuerror_success.erl + + $i "Add the test case to CONCUERROR_TESTS" + $t perl -ni.bak -e 'print;if ($$.==1) {print "CONCUERROR_TESTS += concuerror_success:test\n"}' $(APP)/Makefile + + $i "Confirm that Concuerror completes successfully" + $t $(MAKE) -C $(APP) concuerror $v + + $i "Create a test module with a function that has no local return" + $t printf "%s\n" \ + "-module(concuerror_error)." \ + "-export([test/0])." \ + "test() -> 1 = 2, ok." > $(APP)/test/concuerror_error.erl + + $i "Add the test case to CONCUERROR_TESTS" + $t perl -ni.bak -e 'print;if ($$.==1) {print "CONCUERROR_TESTS += concuerror_error:test\n"}' $(APP)/Makefile + + $i "Confirm that Concuerror errors out" + $t ! $(MAKE) -C $(APP) concuerror $v -- cgit v1.2.3