rems-project / rmem Goto Github PK

I'm trying a very simple program on two processors, something like lock(); var++; unlock();.
The post-condition tests whether mutual exclusion holds. I'm trying to understand the output of the test.

flatOpt gives me the following output:

% flatOpt -interactive false -eager true -loop_limit 2 -random_traces 100 spinlock.litmus
Test spinlock Allowed
Memory-writes=
States 2
10    :>0:X6=1; 1:X6=2; lock=0;  via "0;0;0;4;3;1;1;1;0;0;2;1;0;1;0"
10    :>0:X6=2; 1:X6=1; lock=0;  via "3;3;4;2;2;1;3;4;1;2;0;0;1;0;1;0;0"
Deadlock states 80  via "3;3;3;0;4;0;2;0"
Unhandled exceptions 0

No (allowed not found)
Condition exists (not (lock=0) \/ 0:X6=1 /\ 1:X6=1)
Hash=38aa9d1fdad5a92505f642b7639393de
Observation spinlock Never 0 2 with deadlocks
Runtime: 2.223359 sec

Both observed states are exactly what I expected. But how should I interpret the Deadlock state?

• Are these real deadlocks and the code is unsafe?
• Are these false positives and I can ignore them?
• Or are these potentially dangerous states? How to go from here?

Here is the complete litmus test. It is based on the spinlock of arm-trusted-firmware.

AArch64 spinlock
(* 
 * Critical section with load-/store-exclusive spinlock.
 * https://github.com/ARM-software/arm-trusted-firmware/blob/master/lib/locks/exclusive/aarch64/spinlock.S
 *)
{
    uint32_t lock=0;
    var=0;

    0:X0=lock ;  1:X0=lock ;
    0:X3=var  ;  1:X3=var  ;
}

        P0               |          P1              ;

(* lock ********************************************)
        MOV W2,#1        |          MOV W2,#1       ;
L01:    LDAXR W1,[X0]    |  L11:    LDAXR W1,[X0]   ;
        CBNZ W1,L01      |          CBNZ W1,L11     ;
        STXR W1,W2,[X0]  |          STXR W1,W2,[X0] ;
        CBNZ W1,L01      |          CBNZ W1,L11     ;

(* critical section ********************************)
        LDR W6,[X3]      |          LDR W6,[X3]     ;
        ADD W6,W6,#1     |          ADD W6,W6,#1    ;
        STR W6,[X3]      |          STR W6,[X3]     ;
                          
(* unlock ******************************************) 
        STLR WZR,[X0]    |          STLR WZR,[X0]   ;

exists (lock!=0 \/ (0:X6 = 1 /\ 1:X6 = 1))

Hello,

I am encountering a build error while trying to install rmem with Ocaml 4.07. (I also tried v4.06, but to no avail.)

The build fails at the following command:

../lem/lem -only_changed_output -wl_unused_vars ign -wl_pat_comp ign -wl_pat_exh ign -wl_comp_message ign -wl_rename ign -wl_pat_red ign -outdir build_concurrency_model/ -ocaml build_sail_interp/interp_lib.lem build_sail_interp/interp_interface.lem build_sail_interp/interp_utilities.lem build_sail_interp/interp.lem build_sail_interp/sail_impl_base.lem build_sail_interp/interp_inter_imp.lem build_sail_interp/interp_ast.lem build_sail_interp/instruction_extractor.lem build_sail_shallow_embedding/deep_shallow_convert.lem build_sail_shallow_embedding/sail_values.lem build_sail_shallow_embedding/prompt.lem build_sail2_shallow_embedding/sail2_instr_kinds.lem build_sail2_shallow_embedding/sail2_values.lem build_sail2_shallow_embedding/sail2_operators.lem build_sail2_shallow_embedding/sail2_operators_mwords.lem build_sail2_shallow_embedding/sail2_prompt_monad.lem build_sail2_shallow_embedding/sail2_prompt.lem build_sail2_shallow_embedding/sail2_string.lem src_concurrency_model/utils.lem src_concurrency_model/freshIds.lem build_isa_models/power/power_extras_embed.lem build_isa_models/power/power_embed_types.lem build_isa_models/power/power_embed.lem src_concurrency_model/isaInfoPPCGen.lem build_isa_models/power/power_extras.lem build_isa_models/aarch64/armV8_extras_embed.lem build_isa_models/aarch64/armV8_embed_types.lem build_isa_models/aarch64/armV8_embed.lem src_concurrency_model/isaInfoAArch64.lem build_isa_models/aarch64/armV8_extras.lem src_concurrency_model/isa_stubs/mips/mips_embed_types.lem src_concurrency_model/isa_stubs/mips/mips_embed.lem src_concurrency_model/isa_stubs/mips/isaInfoMIPS.lem src_concurrency_model/isa_stubs/mips/mips_extras.lem build_isa_models/riscv/riscv_extras.lem build_isa_models/riscv/riscv_types.lem build_isa_models/riscv/riscv.lem src_concurrency_model/isaInfoRISCV.lem build_isa_models/x86/x86_extras_embed.lem build_isa_models/x86/x86_embed_types.lem build_isa_models/x86/x86_embed.lem src_concurrency_model/isaInfoX86.lem build_isa_models/x86/x86_extras.lem src_concurrency_model/instructionSemantics.lem src_concurrency_model/events.lem src_concurrency_model/fragments.lem src_concurrency_model/basicTypes.lem src_concurrency_model/regUtils.lem src_concurrency_model/uiTypes.lem src_concurrency_model/params.lem src_concurrency_model/dwarfTypes.lem src_concurrency_model/candidateExecution.lem src_concurrency_model/machineDefTypes.lem src_concurrency_model/machineDefUI.lem src_concurrency_model/machineDefPLDI11StorageSubsystem.lem src_concurrency_model/machineDefFlowingStorageSubsystem.lem src_concurrency_model/machineDefFlatStorageSubsystem.lem src_concurrency_model/machineDefPOPStorageSubsystem.lem src_concurrency_model/machineDefNOPStorageSubsystem.lem src_concurrency_model/machineDefTSOStorageSubsystem.lem src_concurrency_model/machineDefInstructionPredicates.lem src_concurrency_model/machineDefThreadSubsystemUtils.lem src_concurrency_model/machineDefThreadSubsystem.lem src_concurrency_model/machineDefSystem.lem src_concurrency_model/machineDefTransitionUtils.lem src_concurrency_model/promisingViews.lem src_concurrency_model/promisingTransitions.lem src_concurrency_model/promisingUtils.lem src_concurrency_model/promisingThread.lem src_concurrency_model/promisingStorage.lem src_concurrency_model/promising.lem src_concurrency_model/promisingDwarf.lem src_concurrency_model/promisingUI.lem build_isa_models/power/power_toFromInterp.lem build_isa_models/aarch64/armV8_toFromInterp.lem src_concurrency_model/isa_stubs/mips/mips_toFromInterp.lem src_concurrency_model/isa_stubs/riscv/riscv_toFromInterp.lem build_isa_models/x86/x86_toFromInterp.lem File "build_isa_models/riscv/riscv_extras.lem", line 11, character 35 to line 11, character 56 Type error: type mismatch: application expression unit -> _ and Sail2_instr_kinds.barrier_kind

Please find the complete output log here.

Thank you,
Michalis

I'm trying to run this simple example for AArch64:

AArch64 loop
{
    x=0;
    0:X0=x;
}

        P0;
L01:    LDR W1,[X0];
        CBNZ W1,L01;
        MOV W1,#1;
        STR W1,[X0];

exists (x=0)

Since x is initially 0, the conditional branch should be skipped and 1 should be stored in x, AFAICT.

Running rmem/flat in non-interactive mode never terminates. Similarly, the exhaustive search in the interactive mode does not terminate. If I simply auto-step (a) in interactive mode, the execution terminates as expected.

This is how I am calling the rmem tool in non-interactive mode:

flat -interactive false -eager true example.litmus

Am I missing some obvious configuration or step? Do you have any suggestion how to discover what is going on? Thank you.

Note: rmem built with OCaml 4.06.1 at commit 3822f35.

I want to use rmem to verify the execution of a riscv cpu verilog simulation.

I can grab all the required info from the simulation, eg instruction 1 wrote to memory 0x1000/8=1, instruction 2 read from store buffer 0x1000/8=1, instruction 3 read from memory 0x1000/8=1, etc. I then want to check that those simulation results are a valid RVWMO execution.

My idea is to add a step_string instruction to rmem. Given a string argument, it will search the enabled transitions for that string. If it finds one transition that contains that string, then it will take that transition. Eg, one could do

step_string "satisfy memory read by forwarding from writes: (0:3:0):R 0x0000000000001000/8 from (0:2:0):W 0x0000000000001000/8=1"

I can create the above command, and ones like it, directly from a simulation trace and feed it to rmem to check the execution.

Does that sound reasonable? Would you recommend something else?

I've implemented a primitive step_string in rmem myself and it's working on my manually written toy examples.

When building rmem from scratch, it pulls sail from our local repos https://github.com/rems-project/opam-repository/tree/opam2/packages/sail

If it pulls sail=0.13 then a problem can happen, because our repo's opam file is underconstrained, and if opam tries to pull omd=2.0, the build will fail.

We'd like to try some small ELF files with the tool, so I started with a NOP instruction.

It looks like this:

% aarch64-linux-gnu-objdump -D nop.elf

nop.elf:     file format elf64-littleaarch64


Disassembly of section .text.boot:

0000000000080000 <main>:
   80000:	d503201f 	nop

When I run that with flat or flatOpt, the tool terminates with an exception because it tries to fetch the next instruction, but there is none.

Unhandled exceptions 1
1     :>thread 0 instruction 0:2: illegal fetch address exception: 0x0000000000080004 via ""

Executing in the interactive mode, I could see that the NOP instruction was executed as expected.

So, how to properly build an ELF file to run with the tool? I'm sorry if that is a very basic question, but I could not find any specific instructions to do that.

I am unable to execute any of the riscv elf tests on the web interface or the CLI.

For example, if I load the loop5-O0 test on https://www.cl.cam.ac.uk/~sf502/regressions/rmem/, and execute step 20, I get this exception -

0:1    0x01010c (_start) fetch error          
  micro_op_state: MOS_pending_exception decode error: Internal error Type_check.Type_error(_, 0, _)
  waiting to raise an exception
  0 0:1    raise exception: decode error: Internal error Type_check.Type_error(_, 0, _)
          t @ 0x11170
          i @ 0xfffff0003ec

On the CLI, if I take the same loop5-O0 binary (compiled from https://github.com/litmus-tests/litmus-tests-riscv/tree/master/elf-tests/basic), and run ./rmem -model relaxed -model flat -cmds "step 20" I get this exception -

Failure while taking transition (from the state above):                                                                                                                                               
  0:2    register read: cur_privilege = 2b_1'10 from initialstate of 0-1:2b_0'10                                                                                                                      
                                                                                                                                                                                                      
Fail: Pattern match failure at model/riscv_types.sail 78:2 - 82:3. regval_privilege                                                                                                                   
                                                                                                                                                                                                      
Fatal error: exception Failure("Fail: Pattern match failure at model/riscv_types.sail 78:2 - 82:3. regval_privilege")                                                                                 
Raised at file "list.ml", line 187, characters 10-25                                                                                                                                                  
Called from file "src_top/pp.ml", line 359, characters 4-42   

I was able to fix the problem on the CLI with the following change -
VarunKoyyalagunta@8737b47

I can create a PR for that if that is the appropriate fix. I just copied the initial cur_privilege and mstatus settings from

I want to run rmem in a scripted batch mode, by creating a file containing a list of commands and be able to do something like this -

cat file.cmd | ./rmem ... | tee log

(It's more complicated by the fact that I'm running the ./rmem ... part inside a container, but that doesn't really matter)

If I compile with UI=headless, rmem accepts input from a STDIN pipe. However I can't redirect STDOUT. I get the following error -

Output is not a terminal, '-interactive true' is not allowed.
  Use '-interactive false'

Removing the check, like so, achieves what I want -
VarunKoyyalagunta@8f0da61

I thought of creating some sort of -batch switch instead to override the check, but I'm not sure how useful the check is to begin with and removing it seemed easier.

If the above change is okay, I can create a PR. Or, if you prefer an additional switch like -batch, I can code that.

I failed to install dependencies with the following error log:

$ opam --version 
2.0.5

$ ocamlc --version
4.10.0

$ opam install . 
[rmem.0.1] no changes from git+file:///kaist-cp-home/jeehoon.kang/Works/rmem#master
Sorry, no solution found: there seems to be a problem with your request.

No solution found, exiting

I wonder if this error is familiar to the developers. Thanks!

If I understand correctly, this repo implements (among other things) Section 6.2-6.5 of the paper Simplifying ARM Concurrency: Multicopy-atomic Axiomatic and Operational Models for ARMv8 in Ocaml.
Is there a logical formalization of the inter-instruction semantics described in that part of the paper? If not, is there a way to extract it somehow from this repo?

Is it possible that in thread 1, the register x2 has value 2 and x1 has value 4?
if not, how does the flat model (the operation model as described in  Section 6.2-6.5 of the paper Simplifying ARM Concurrency: Multicopy-atomic Axiomatic and Operational Models for ARMv8) rule it out?
The description there of reading from memory seems simple:

I'm trying to understand whether or when it is feasible to perform exhaustive tests with rmem. So far my experience was that showing something is wrong is pretty quick (which is awesome), but showing that something is correct often does not terminate.

I'm trying simple pieces like lock(); var++; unlock();. One actual litmus test I am using is below.

For example,

• flatOpt with loop-limit terminates 10000 random traces of this code in 25 minutes, which is fine. But I guess that I can make no claim about the coverage of such test. The actual number of executions can only be counted by exhaustively running the model. Is that right?
• exhaustive testing this code with flatOpt does not terminate after running for 2 days. Btw, the tool seem to use only a single core of the host. Is that by design or am I missing some configuration?
• I had no luck with promisingOpt. It consumes much more memory than flatOpt and does not terminate even for a few random traces.
• I also tried -eager_fetch_unmodified, which then quickly terminates but does not find all final states. I guess I don't understand what this option does.

So, I am wondering how to use rmem to verify code that we believe to be correct. Are people doing this? Do you have any suggestion how to tackle an exhaustive verification of the following example?

AArch64 spinlock
(* 
 * Critical section with load-/store-exclusive spinlock.
 * https://github.com/ARM-software/arm-trusted-firmware/blob/master/lib/locks/exclusive/aarch64/spinlock.S
 *)
{
    uint32_t lock=0;
    var=0;

    0:X0=lock ;  1:X0=lock ;
    0:X3=var  ;  1:X3=var  ;
}

        P0               |          P1              ;

(* lock ********************************************)
        MOV W2,#1        |          MOV W2,#1       ;
L01:    LDAXR W1,[X0]    |  L11:    LDAXR W1,[X0]   ;
        CBNZ W1,L01      |          CBNZ W1,L11     ;
        STXR W1,W2,[X0]  |          STXR W1,W2,[X0] ;
        CBNZ W1,L01      |          CBNZ W1,L11     ;

(* critical section ********************************)
        LDR W6,[X3]      |          LDR W6,[X3]     ;
        ADD W6,W6,#1     |          ADD W6,W6,#1    ;
        STR W6,[X3]      |          STR W6,[X3]     ;
                          
(* unlock ******************************************) 
        STLR WZR,[X0]    |          STLR WZR,[X0]   ;

exists (lock!=0 \/ (0:X6 = 1 /\ 1:X6 = 1))

If you run in the web-interface the MP litmus test from the library (rmem link), you can see in the Graph pane, that the 'co' edge from the initial value of 'x' to the first store of 'x' is coming out of what looks like the initial value of 'y'.

The root of the problem is that the .dot file rmem generates includes HTML-like labels with PORT attribute that includes ':'. For example: <TD PORT="w(1000:1:0)">.
neato silently ignores those ports when placing edges. So, for example this:

/* coherence */
"i1000:0":"w(1000:1:0)" -> "i0:1":"w(0:1:0)" [...]

is actually seen by neato as this:

/* coherence */
"i1000:0" -> "i0:1" [...]

Hence, the 'co' edge goes out from the big node that is wrapped around both values of 'x' and 'y', instead of going out of 'x'.

The tikz backend (src_top/tikz.ml) had a similar problem. This is why it uses pp_tikz_pretty_ioid, instead of Pp.pp_prettey_ioid.

IIUC, ARMv8-A LSE2 (Large System Extension 2) enables atomic misaligned reads that "fit in cachelines", and that seems to affect the model in minor ways — it seems the "storage" model reflects properties of caches and not just RAM.

For instance, a LDP instruction can read the the 64-bit value at address range [0x4, 0x12[ atomically — but only if the memory has inner & outer writeback cacheability.

• If your RAM model forbids such a misaligned access, LSE2 requires allowing that, at least sometimes.
• If your RAM model always allows such a misaligned access, no change is needed for LSE2 — that just seems a bit odd, and it means storage behavior accounts for some effects of caches as well.

References.

This is documented in prose in DDI0487 I.a, Sec. B2.5.2 Alignment of data accesses.

This is also documented in the DDI0487 I.a pseudocode (but not in DDI0487 G.a): function aarch64/functions/memory/AArch64.MemSingle (in Appendix J-1) will let CheckSingleAccessAttributes decide to split the access.

In section 6.4 of Simplifying ARM Concurrency: Multicopy-atomic Axiomatic and Operational Models for ARMv8, the inter-instruction semantics talks about forwarding writes to reads, e.g.:

But it doesnt seem to talk about forwarding reads to other reads of the same location. Does ARM do that? if so, how does SAIL+RMEM capture it? More concretely, consider the following example:
LD 300 x0; LD 300; x1. Must the CPU issue 2 read requests to the memory? If not, how does SAIL+RMEM model the "forwarding" of the value read in one instruction to the other?

Does the promising model work with elf files? I have been trying with interactive and non-interactive mode, but nothing seems to actually happen. My start code looks like this:

_start:
    // start 3 threads
    ldr x0,=run
    .word 0xd50bb003
    ldr x0,=run
    .word 0xd50bb003
    ldr x0,=run
    .word 0xd50bb003

    // call run as thread 0 (total = 4 threads)
    // prototype: void run(unsigned int tid);
    mov x0, #0
    b run

And it has been working with flat. Is this also ok for promising or should I do something else?