>From 53df3405f334e7cda1d650fefbf5fba416aa4abe Mon Sep 17 00:00:00 2001 From: Akira Yokosawa <akiyks@xxxxxxxxx> Date: Wed, 22 Nov 2017 20:08:09 +0900 Subject: [PATCH] CodeSamples/formal/herd: Add existence check of memory model If any of the necessary files is lacking, output a message to give instructions for preparation of the memory model. Suggested-by: Paul E. McKenney <paulmck@xxxxxxxxxxxxxxxxxx> Signed-off-by: Akira Yokosawa <akiyks@xxxxxxxxx> --- CodeSamples/formal/herd/.gitignore | 1 + CodeSamples/formal/herd/Makefile | 28 +++++++++++++++++++++++++--- 2 files changed, 26 insertions(+), 3 deletions(-) diff --git a/CodeSamples/formal/herd/.gitignore b/CodeSamples/formal/herd/.gitignore index c7ba463..e0ad195 100644 --- a/CodeSamples/formal/herd/.gitignore +++ b/CodeSamples/formal/herd/.gitignore @@ -2,3 +2,4 @@ *.herd klitmus klitmus.tar +memory-model diff --git a/CodeSamples/formal/herd/Makefile b/CodeSamples/formal/herd/Makefile index 9df6e65..1abe5c7 100644 --- a/CodeSamples/formal/herd/Makefile +++ b/CodeSamples/formal/herd/Makefile @@ -9,14 +9,24 @@ # # run-herd7-bench: Run benchmark tests of herd7 itself # -# Note: LKMM model is assumed to reside in a directory next to perfbook's -# local repository. +# Note: There need to be a symbolic link "memory-model" under +# CodeSamples/formal/herd for herd7 to work. +# The memory model is available at the git archive: +# https://github.com/aparri/memory-model.git. +# Make sure the symbolic link points to the actual directory. +# Alternatively, you can copy the files listed in LKMM_FILES to +# a subdirectory "memory-model". +# +# klitmus7 doesn't require the memory model. # # Copyright (C) Akira Yokosawa, 2017 # # Authors: Akira Yokosawa <akiyks@xxxxxxxxx> -LKMM_DIR := ../../../../memory-model +LKMM_DIR := memory-model +LKMM_FILES := linux-kernel.bell linux-kernel.cat linux-kernel.cfg \ + linux-kernel.def linux-kernel-hardware.cat lock.cat +LKMM_LIST := $(addprefix $(LKMM_DIR)/,$(LKMM_FILES)) HERD_DIR := $(shell pwd) HERD7_CMD := $(shell which herd7) KLITMUS7_CMD := $(shell which klitmus7) @@ -41,6 +51,18 @@ run-herd7: $(LITMUS7_HERD_OUT) run-herd7-bench: $(HERD_BENCH_OUT) +$(LKMM_LIST): + @echo "#####################################################" + @echo "### Please prepare Linux Kernel Memory Model. ###" + @echo "### You can get it at the git archive: ###" + @echo "### https://github.com/aparri/memory-model.git ###" + @echo "### ###" + @echo "### Refer to comment in Makefile for more info. ###" + @echo "#####################################################" + @exit 1 + +$(LITMUS7_HERD_OUT) $(HERD_BENCH_OUT): $(LKMM_LIST) + $(LITMUS7_HERD_OUT): %.out: %.herd cd $(LKMM_DIR); herd7 -conf linux-kernel.cfg $(HERD_DIR)/$< > $(HERD_DIR)/$@ -- 2.7.4 -- To unsubscribe from this list: send the line "unsubscribe perfbook" in the body of a message to majordomo@xxxxxxxxxxxxxxx More majordomo info at http://vger.kernel.org/majordomo-info.html
