MTA Does Not Terminate on Large Project

[dylanjwolff]

Hi @yuleisui,

Thanks for your help on #1548!

I'm now trying to run MTA on that same bitcode file (a SQLite stress test), but it is taking more than 24 hours (!). It is a relatively large program, so I'm not sure if this is expected behavior or maybe a performance bug. I have tried on some other larger programs though (>10k LOC), and many of them seem to take more than 24 hours to terminate.

Here is the command I am using:

mta -dump-icfg -race -stat=false labeled.bc

If it is just because of fundamental scalability issues, is there any way to easily relax the analysis to trade off precision on these larger projects such that the analysis can terminate in a reasonable amount of time? For my use case, it is OK if there are a larger number of false positives, but ideally the analysis would finish within a few minutes.

I've tried commenting out most of the functionality in LockAnalysis.cpp, but even that alone doesn't seem to be enough to allow it to terminate quickly.

I'd appreciate any guidance you might have on this. Also happy to help debug if this looks like a bug to you.

Thanks!

labeled.bc.tar.gz

OS: Ubuntu 22.04.5 LTS x86_64
Kernel: 6.8.0-45-generic
CPU: Intel i7-10700 (16) @ 4.800GHz
Memory: 15700MiB

[LimbicSys]

I have tried MTA on some real world projects. It is slow on large project. It may take 2~3 days (or more) on a 10k LOC project.

[LimbicSys]

I have tried MTA on some real world projects. It is slow on large project. It may take 2~3 days (or more) on a 10k LOC project.

I guess that the pointer analysis take too much time. Getting an only ICFG of a large project is quite fast.

[dylanjwolff]

I did some light profiling (please take with a grain of salt), and there appear to be multiple bottlenecks.

The first is that just constructing the TCT takes a very long time for large programs.

This seems to mostly be due to the context sensitivity.

If we remove context-sensitivity, this phase of the analysis wil terminate within a reasonable amount of time (a couple of hours). However, for computing race pairs, again there is a bottleneck. Since the race pair computation is pairwise, there are M*N checks for may-happen-in-parallel etc., which is too much for programs where M and N are on the order of 600k loads+stores.

As a note, I am on the latest release version SVF-3.0 -- I realized that I missed adding that to the original issue