rems-project / rmem

rmem public repo
Other
40 stars 9 forks source link

Promising with elf files #8

Closed db7 closed 5 years ago

db7 commented 5 years ago

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?

cp526 commented 5 years ago

The Promising model works with elf files, but so far did not support dynamically creating threads. I have just finished adding a mechanism that allows dynamically starting threads to Promising. If you run your test with the "-elf_threads" option and an up-to-date checkout of Promising this should work now as in Flat.

Two things to note: (1) this is just newly added and not tested much. (2) currently the user-interface may be a bit confusing: when Promising starts a new thread --- this is done via a special kind of promise --- this is recorded in part of the storage subsystem state (recording that the thread is now active) but not immediately reflected in the thread subsystem state of the activated thread, other than that it will now have transitions available.

db7 commented 5 years ago

@cp526, that is great! I will give a try. So if I understood correctly, I can run exactly the same code (with the special instruction 0xd50bb003). Thank you.

cp526 commented 5 years ago

Yes, the same code using that magic instruction should work. Again, this has not been tested much so far, so hopefully it'll work as expected for your example.

db7 commented 5 years ago

Indeed, I got problems running examples. Here is the smallest case which gets stuck for me:

_start:
        ldr x0,=main
        .word 0xd50bb003

main:   // all threads start here
        ldr x1,=var
        ldr w2,[x1]   // loads var
        sub w2,w2,#1  // decrement value
        str w2,[x1]   // stores back to var
        ret

.section ".data"
var:
    .word 0xDEADBEEF
    .word 0x00000000

I start this example like this:

promisingOpt -interactive false -elf_threads 2 -loop_limit 3 threads.elf

And my linker.ld looks like this:

SECTIONS
{
    . = 0x80000;
    .text : { *(.text) }
    .data : { *(.data) }
}

With this example in the interactive mode, I can see the list of promises increasing without end:

    0     0:0    promise write: (0:524336:0):W 0x0000000000080030 (var)/4=0xdeadbeea. Required view: 14 ***
    1     0:0    promise write: (0:524336:0):W 0x0000000000080030 (var)/4=0xdeadbeeb. Required view: 13    
    2     0:0    promise write: (0:524336:0):W 0x0000000000080030 (var)/4=0xdeadbeec. Required view: 12    
    3     0:0    promise write: (0:524336:0):W 0x0000000000080030 (var)/4=0xdeadbeed. Required view: 11    
    4     0:0    promise write: (0:524336:0):W 0x0000000000080030 (var)/4=0xdeadbeee. Required view: 5    
    5     1:0    promise write: (1:524336:0):W 0x0000000000080030 (var)/4=0xdeadbeea. Required view: 14    
    6     1:0    promise write: (1:524336:0):W 0x0000000000080030 (var)/4=0xdeadbeeb. Required view: 13    
    7     1:0    promise write: (1:524336:0):W 0x0000000000080030 (var)/4=0xdeadbeec. Required view: 12    
    8     1:0    promise write: (1:524336:0):W 0x0000000000080030 (var)/4=0xdeadbeed. Required view: 11    
    9     1:0    promise write: (1:524336:0):W 0x0000000000080030 (var)/4=0xdeadbeee. Required view: 5    

And it keeps growing. I guess it won't terminate. The same elf file finishes in less than a second with flatOpt. Also, if I change the example not to store anything to memory, promisingOpt quickly finishes as expected.

Should I use some extra command line option? Or do you have any other suggestion?

cp526 commented 5 years ago

Thanks for reporting this, this does look odd. What's the assembler command you're running, so I can reproduce your binary?

db7 commented 5 years ago

Thanks for taking a look. Here are the commands:

aarch64-linux-gnu-as -c threads.S -o threads.o
aarch64-linux-gnu-gcc -Wl,--build-id=none -nostdlib -nostartfiles \
    threads.o -T linker.ld -o threads.elf

Perhaps I did something wrong while updating rmem? I updated sail2 and recompiled and updated rmem and recompiled.

cp526 commented 5 years ago

I think I found the error in Promising I introduced when adding the thread start mechanism. On my machine the infinite looping does not show up for this example any more and the program terminates quickly.

db7 commented 5 years ago

It started working for me too. Thank you!