Alloc-free dev by CapZTr · Pull Request #1 · CapZTr/Dat3M

CapZTr · 2025-05-14T08:55:26Z

No description provided.

* init alias analysis for alloc Signed-off-by: Tianrui Zheng <tianrui.zheng@huawei.com> * add MemFree events to the test Signed-off-by: Tianrui Zheng <tianrui.zheng@huawei.com> * add first test for alias analysis Signed-off-by: Tianrui Zheng <tianrui.zheng@huawei.com> * add second test for alias analysis Signed-off-by: Tianrui Zheng <tianrui.zheng@huawei.com> * improve field insensitive for alloc Signed-off-by: Tianrui Zheng <tianrui.zheng@huawei.com> * add third test for alias analysis Signed-off-by: Tianrui Zheng <tianrui.zheng@huawei.com> * add alias analysis for free events Signed-off-by: Tianrui Zheng <tianrui.zheng@huawei.com> * use alias analysis for alloc and free in relation analysis Signed-off-by: Tianrui Zheng <tianrui.zheng@huawei.com> * change native relation analysis Signed-off-by: Tianrui Zheng <tianrui.zheng@huawei.com> * change logic of mustAlias Signed-off-by: Tianrui Zheng <tianrui.zheng@huawei.com> * Using stack pointer in alloc tests * change exception type Signed-off-by: Tianrui Zheng <tianrui.zheng@huawei.com> * Add full alias analysis Signed-off-by: Tianrui Zheng <tianrui.zheng@huawei.com> * Add object alias for alloc -> memory event Signed-off-by: Tianrui Zheng <tianrui.zheng@huawei.com> * Add alloc and free to alias graph Signed-off-by: Tianrui Zheng <tianrui.zheng@huawei.com> --------- Signed-off-by: Tianrui Zheng <tianrui.zheng@huawei.com> Co-authored-by: Tianrui Zheng <tianrui.zheng@huawei.com> Co-authored-by: Natalia Gavrilenko <natgavrilenko@gmail.com>

Signed-off-by: Tianrui Zheng <tianrui.zheng@huawei.com>

natgavrilenko · 2025-05-14T09:10:21Z

dartagnan/src/test/java/com/dat3m/dartagnan/llvm/AllocFreeTest.java

+                .withConfig(configuration)
+                .withTarget(target);
+        Program program = new ProgramParser().parse(new File(getTestResourcePath("alloc/" + name + ".ll")));
+        Wmm mcm = new ParserCat().parse(new File(getRootPath("cat/vmm.cat")));


Let's add tests for all the three models: vmm, rc11, and c11. I think expected results should be different for all of them, so, instead of listing all variations explicitly, we can loop through the models or create a separate unit test for each model.

All the tests we have so far have same results for the three models. Do you mean we will have some tests that pass for some models but fail for others?

I mean that it is very unlikely that we will have tests that should pass for one model and fail for the other, so we can use the same expected results for all models.

I see.

I think expected results should be different for all of them

It confused me a bit :-)

natgavrilenko · 2025-05-14T09:11:00Z

dartagnan/src/test/java/com/dat3m/dartagnan/llvm/AllocFreeTest.java

@@ -0,0 +1,117 @@
+package com.dat3m.dartagnan.c;


The package is "com.dat3m.dartagnan.llvm"

natgavrilenko · 2025-05-14T09:11:39Z

cat/c11.cat

+flag ~empty (allocmem \ hb) as use-before-alloc
+flag ~empty ((allocmem^-1 ; (allocptr & (ALLOC * FREE))) \ hb) as use-after-free
+
+// TODO: Non-monotonic! (see ThreadCreation class)


Thread join has been fixed, so this TODO can be removed for all three models

natgavrilenko · 2025-05-14T09:13:08Z

dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/MemFree.java

+import java.util.HashSet;
+import java.util.Set;
+
+// TODO: Consistent naming. Should we rename relation 'Free' into FreeRel?


Let's align the naming and remove the TODO. Any reasonable naming of your choice should be fine.

Renamed Alloc to MemAlloc

natgavrilenko · 2025-05-14T09:14:42Z

dartagnan/src/main/java/com/dat3m/dartagnan/encoding/NonTerminationEncoder.java

        - Side-effectful non-termination requires at least one infix iteration
        - Side-effect-free non-termination causes exactly one suffix iteration.
     */
-    private BooleanFormula encodeInfixSuffixDecomposition() {


All these methods can be changed back to private

natgavrilenko · 2025-05-14T09:15:08Z

dartagnan/src/main/java/com/dat3m/dartagnan/encoding/PropertyEncoder.java

        BooleanFormula encoding = (specType == Property.Type.SAFETY) ?
                encodePropertyViolations(properties) : encodePropertyWitnesses(properties);
-        if (!program.getFormat().equals(LLVM) || properties.contains(TERMINATION)) {
+        // if (!program.getFormat().equals(LLVM) || properties.contains(TERMINATION)) {


Can be changed back

natgavrilenko · 2025-05-14T09:17:24Z

dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/ThreadCreation.java

 import com.dat3m.dartagnan.program.Thread;
 import com.dat3m.dartagnan.program.*;
 import com.dat3m.dartagnan.program.event.*;
+import com.dat3m.dartagnan.program.event.core.Assume;


Unused import

natgavrilenko · 2025-05-14T09:28:17Z

dartagnan/src/main/java/com/dat3m/dartagnan/wmm/Wmm.java

+            //         getOrCreatePredefinedRelation(IDDTRANS),
+            //         addDefinition(product(newRelation(), Tag.MEMORY, Tag.MEMORY))
+            // );
+            case DATA -> {


This works correctly but doesn't look very clean. I think at this point we should consider if:

Alloc and Free events should have Tag.MEMORY

Alloc and Free events should inherit MemoryEvent or MemoryCoreEvent.

I didn't look into this myself yet, but we should definitely check what would be the implications of this. It might be that it will also make alias analysis a bit cleaner and give us ordering via the co relation (if Alloc and Free are a part of the co chain). It might be also that it is not going to work for some reason.

We can also change Tag.MEMORY to Tag.VISIBLE, and it should include all the necessary events

Signed-off-by: Tianrui Zheng <tianrui.zheng@huawei.com>

natgavrilenko · 2025-07-23T23:11:08Z

Could you change this merge request to use development branch as a base? Otherwise, there are many changes that are not related to alloc-free

Signed-off-by: Tianrui Zheng <tianrui.zheng@huawei.com>

natgavrilenko · 2025-07-23T23:08:26Z

dartagnan/src/test/resources/lfds/dglm.ll

@@ -1,51 +1,49 @@
-; ModuleID = 'dglm.c'
-source_filename = "dglm.c"
+; ModuleID = 'benchmarks/lfds/dglm.c'


We also need to update .ll files for dglm-CAS-relaxed, ms-CAS-relaxed, and trebier-CAS-relaxed. It should probably be possibly to figure out what exactly was relaxed if you compare the relaxed .ll file with a the original non-relaxed .ll file.

natgavrilenko · 2025-07-23T23:09:12Z

dartagnan/src/test/resources/locks/clh_mutex.ll

@@ -1,376 +1,307 @@
-; ModuleID = '/home/ponce/git/Dat3M/output/clh_mutex.ll'
-source_filename = "/home/ponce/git/Dat3M/benchmarks/locks/clh_mutex.c"
+; ModuleID = 'benchmarks/locks/clh_mutex.c'


Same here, we should also update the alternative acq2rx files

natgavrilenko · 2025-07-24T08:14:15Z

benchmarks/alloc/test1_err_address.c

+    arr[0] = 0;
+    arr[1] = 1;
+
+	return NULL;


Minor thing: it looks like the indentation is too large here and in several other places

natgavrilenko · 2025-07-24T08:34:39Z

benchmarks/alloc/test1_ok_2.c

@@ -0,0 +1,26 @@
+#include <stdlib.h>


Since all tests here start with 'test1_', we can rename them to just 'test_'

natgavrilenko · 2025-07-24T08:57:25Z

benchmarks/lfds/dglm.h

 _Atomic(Node *) Tail;
 _Atomic(Node *) Head;

+#define RETIRE_THRESHOLD 10


I think it is better not to modify the original algorithm with our custom retirement method but do the following:

Keep a 'normal' free and add a comment that it should retire instead

For the VMMLFDSTest which fails, splits it into three tests: one for PROGRAM_SPEC, one for TERMINATION, and one for CAT_SPEC.

For the CAT_SPEC version of the tests, change expected result to 'FAIL' and add a comment that it fails use-after-free because it requires safe memory reclamation.

Now we need AllocMemGraph and AllocPtrGraph because lack of these two makes testing with only one property PROGRAM_SPEC or TERMINATION impossible.

natgavrilenko · 2025-07-24T09:06:01Z

dartagnan/src/main/java/com/dat3m/dartagnan/encoding/PropertyEncoder.java

-            encoding = bmgr.and(encoding, encodeProgramTermination());
+            Event termination = program.getThreadEvents(Termination.class).stream().findFirst()
+                   .orElseThrow(() -> new IllegalArgumentException("Malformed program: missing the termination event"));
+           encoding = bmgr.and(encoding, context.execution(termination));


indentation

natgavrilenko · 2025-07-24T09:19:35Z

dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/alias/FieldSensitiveAndersen.java

-        ImmutableSet.Builder<Location> addresses = ImmutableSet.builder();
-        Collector collector = new Collector(e.getAddress());
-        addresses.addAll(collector.address());
+    protected ImmutableSet<Location> getAddressSpace(Event e) {


Can be a private method

natgavrilenko · 2025-07-24T09:36:49Z

dartagnan/src/main/java/com/dat3m/dartagnan/wmm/analysis/LazyRelationAnalysis.java

+        }
+
+        @Override
+        // TODO: May and must sets of AllocMem can become very large for some programs.


Maybe we can also try to fix this. As far as I see, in the alias analysis, the only not thread-safe part is the EqualityAliasAnalysis (assuming that it can be called from different threads only after the initialization stage).

The problem is that EqualityAliasAnalysis computes trueSet and falseSet on demand, and that's why it can have a concurrent modification. If we precompute that sets in the constructor (and actually we will only need the trueSet), then it should be safe to use the lazy relation analysis here. Looks like it is a relatively small change that can solve a potentially huge performance issue.

natgavrilenko · 2025-07-24T09:49:17Z

dartagnan/src/main/java/com/dat3m/dartagnan/wmm/Wmm.java

+            // );
+            case DATA -> {
+                Relation mm = addDefinition(product(newRelation(), Tag.MEMORY, Tag.MEMORY));
+                Relation am = addDefinition(product(newRelation(), Tag.ALLOC, Tag.MEMORY));


We can combine tags in a filter instead of creating a separate relation for each tag, something like this

case DATA -> intersection(r, getOrCreatePredefinedRelation(IDDTRANS),
addDefinition(new CartesianProduct(newRelation(),
Filter.union(Filter.byTag(Tag.MEMORY), Filter.byTag(Tag.ALLOC)),
Filter.byTag(Tag.MEMORY))));

Please also delete the commented out code

natgavrilenko · 2025-07-24T09:54:07Z

dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/NonterminationDetection.java

                    .forEach(this::instrumentLoop);
        }

+        program.addTerminationThread();


Ideally, we should optimize this and create a a termination thread only when really needed:

the original condition when encodeProgramTermination() was called in PropertyEncoder, or

if property is CAT_SPEC and there is at least one Alloc event in the program

But I don't immediately see what would be an elegant way to get verification property in a ProgramProcessor. I will try to find a clean solution for this.

Signed-off-by: Tianrui Zheng <tianrui.zheng@huawei.com>

natgavrilenko and others added 11 commits May 13, 2025 14:26

Alloc-free verification prototype

35ca9fc

Using stack pointer in alloc tests

3940bb8

Init setup

20e84e4

Signed-off-by: Tianrui Zheng <tianrui.zheng@huawei.com>

Add Alloc and MemFree to witness for debugging

ddc0e11

Signed-off-by: Tianrui Zheng <tianrui.zheng@huawei.com>

Modified some memory models and tests

8631ddc

Signed-off-by: Tianrui Zheng <tianrui.zheng@huawei.com>

Fix event and relation extraction of alloc-free for witness

44ead61

Signed-off-by: Tianrui Zheng <tianrui.zheng@huawei.com>

Modify some relation and constraint definitions

e5d6a28

Signed-off-by: Tianrui Zheng <tianrui.zheng@huawei.com>

Merge development into this branch

8ff67e2

Signed-off-by: Tianrui Zheng <tianrui.zheng@huawei.com>

Remove unnecessary definition

5f7440f

Signed-off-by: Tianrui Zheng <tianrui.zheng@huawei.com>

Clean c11 and rc11

9803e52

Signed-off-by: Tianrui Zheng <tianrui.zheng@huawei.com>

natgavrilenko reviewed May 14, 2025

View reviewed changes

Tianrui Zheng added 9 commits May 14, 2025 17:05

Modify as comments

0659c5e

Signed-off-by: Tianrui Zheng <tianrui.zheng@huawei.com>

Clean code to prepare rebase

616dfda

Signed-off-by: Tianrui Zheng <tianrui.zheng@huawei.com>

Merge remote-tracking branch 'upstream/development' into alloc-free-dev

ec9717e

Fix merging

4de382e

Signed-off-by: Tianrui Zheng <tianrui.zheng@huawei.com>

Merge remote-tracking branch 'upstream/development' into alloc-free-dev

fd2593f

Fix CI tests: Attempt 1

d752cab

Signed-off-by: Tianrui Zheng <tianrui.zheng@huawei.com>

By Natalia: Add Termination event

89a4219

Signed-off-by: Tianrui Zheng <tianrui.zheng@huawei.com>

Fix CI tests

5d21aee

Signed-off-by: Tianrui Zheng <tianrui.zheng@huawei.com>

Fix CI tests

cd4a5c1

Signed-off-by: Tianrui Zheng <tianrui.zheng@huawei.com>

Merge remote-tracking branch 'upstream/development' into alloc-free-dev

702527a

CapZTr changed the base branch from master to development July 24, 2025 06:37

Fix bugs from merge

f21d510

Signed-off-by: Tianrui Zheng <tianrui.zheng@huawei.com>

natgavrilenko reviewed Jul 24, 2025

View reviewed changes

Tianrui Zheng added 4 commits August 1, 2025 16:32

Add AllocPtrGraph & AllocMemGraph, modify as comments

02998bb

Signed-off-by: Tianrui Zheng <tianrui.zheng@huawei.com>

Reverse vmm.cat

1cdc4c3

Signed-off-by: Tianrui Zheng <tianrui.zheng@huawei.com>

Merge remote-tracking branch 'upstream/development' into alloc-free-dev

5f715e1

Fix bugs from merge

01e6ac1

Signed-off-by: Tianrui Zheng <tianrui.zheng@huawei.com>

Tianrui Zheng added 15 commits August 7, 2025 10:30

Remove vmm from AllocFreeTest

e602036

Signed-off-by: Tianrui Zheng <tianrui.zheng@huawei.com>

Add DI source location for frees

3a08b77

Signed-off-by: Tianrui Zheng <tianrui.zheng@huawei.com>

Add MemAlloc & MemFree to witness

2b60b6c

Signed-off-by: Tianrui Zheng <tianrui.zheng@huawei.com>

Remove unused imports

f4ca35d

Signed-off-by: Tianrui Zheng <tianrui.zheng@huawei.com>

Merge remote-tracking branch 'upstream/development' into alloc-free-dev

e48a53f

Make MemAlloc and MemFree extend GenericMemoryEvent

8d8ca49

Signed-off-by: Tianrui Zheng <tianrui.zheng@huawei.com>

Remove M tag when copy alloc

efa54cc

Signed-off-by: Tianrui Zheng <tianrui.zheng@huawei.com>

Add HeapAlloc

4c531d7

Signed-off-by: Tianrui Zheng <tianrui.zheng@huawei.com>

Add HeapAlloc class

944045f

Signed-off-by: Tianrui Zheng <tianrui.zheng@huawei.com>

Revert to efa54cc

946bf92

Signed-off-by: Tianrui Zheng <tianrui.zheng@huawei.com>

Make MemAlloc & MemFree extend AbstractMemoryCoreEvent

f1a05c6

Signed-off-by: Tianrui Zheng <tianrui.zheng@huawei.com>

Use LazyEventGraph for loc and allocMem in LazyRelationAnalysis

1d49035

Signed-off-by: Tianrui Zheng <tianrui.zheng@huawei.com>

Fix EqualityAliasAnalysis

2404a04

Signed-off-by: Tianrui Zheng <tianrui.zheng@huawei.com>

Fix EqualityAliasAnalysis

5d28e57

Signed-off-by: Tianrui Zheng <tianrui.zheng@huawei.com>

Small change to LazyRelationAnalysis

d7b7b4e

Signed-off-by: Tianrui Zheng <tianrui.zheng@huawei.com>

Conversation

CapZTr commented May 14, 2025

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

natgavrilenko commented Jul 23, 2025

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants