ltsmin does not compile natively on ARM due to hard coded assembly

[mlaveaux]

The ltsmin toolset does not claim compatibility with ARM processors, but since I was a bit caught off guard when preparing an artifact that contained ltsmin I thought it would be good to document this somewhere. I used emulation to get around the problem. The issue seems to be some hard coded instructions in atomics.h:

ltsmin/src/mc-lib/atomics.h

Lines 32 to 38 in 07f9bf8

	#define mfence() { asm volatile("mfence" ::: "memory"); }
	/* Compile read-write barrier */
	#define compile_barrier() asm volatile("": : :"memory")
	/* Pause instruction to prevent excess processor bus usage */
	#define cpu_relax() asm volatile("pause\n": : :"memory")

.

See the compilation errors below:

...
66.24 libtool: compile:  gcc -DHAVE_CONFIG_H -I. -I../../src/hre -I../../src -I../../src -I../../lib -I../../lib -g -O2 -W -Wall -pipe -c bitvector-ll.c -o bitvector-ll.o
66.24 libtool: compile:  gcc -DHAVE_CONFIG_H -I. -I../../src/hre -I../../src -I../../src -I../../lib -I../../lib -g -O2 -W -Wall -pipe -c cctables.c -o cctables.o
66.25 libtool: compile:  gcc -DHAVE_CONFIG_H -I. -I../../src/hre -I../../src -I../../src -I../../lib -I../../lib -g -O2 -W -Wall -pipe -c clt_table.c -o clt_table.o
66.25 libtool: compile:  gcc -DHAVE_CONFIG_H -I. -I../../src/hre -I../../src -I../../src -I../../lib -I../../lib -g -O2 -W -Wall -pipe -c dbs-ll.c -o dbs-ll.o
66.28 {standard input}: Assembler messages:
66.28 {standard input}:272: Error: unknown mnemonic `pause' -- `pause'
66.28 {standard input}:387: Error: unknown mnemonic `pause' -- `pause'
66.28 {standard input}:654: Error: unknown mnemonic `pause' -- `pause'
66.28 make[2]: *** [Makefile:1672: cctables.lo] Error 1
66.28 make[2]: *** Waiting for unfinished jobs....
66.31 {standard input}: Assembler messages:
66.31 {standard input}:651: Error: unknown mnemonic `mfence' -- `mfence'
66.32 make[2]: Leaving directory '/root/ltsmin/src/mc-lib'
66.32 make[2]: *** [Makefile:1672: clt_table.lo] Error 1
66.32 make[1]: *** [Makefile:1669: install-recursive] Error 1
66.32 make[1]: Leaving directory '/root/ltsmin/src'
66.32 make: *** [Makefile:1750: install-recursive] Error 1

[trolando]

The mfence and compile_barrier can be done with C11 atomics nowadays...

#define mfence() atomic_thread_fence(memory_order_seq_cst)
#define compile_barrier() atomic_signal_fence(memory_order_seq_cst);

should do it...
the signal fence is compiler only.

Now for the pause, there's this alternative:

#if defined(__x86_64__) || defined(__i386__) || defined(_M_IX86) || defined(_M_X64)
  #include <immintrin.h>
  #define cpu_relax() _mm_pause()
#elif defined(__aarch64__) || defined(__arm__) || defined(_M_ARM) || defined(_M_ARM64)
  #define cpu_relax() __asm__ volatile("yield" ::: "memory")
#else
  #define cpu_relax() atomic_signal_fence(memory_order_seq_cst)
#endif