search

goblint / bench

The benchmark suite
4 stars 5 forks source link

Add Linux net driver benchmarks from Locksmith papers #24

Open sim642 opened 2 years ago

sim642 commented 2 years ago

Goblint's analysis for all of them is unsound because the unknown register_netdev doesn't spawn all the operation functions since they've been written through an unknown pointer.

sim642 commented 2 years ago

There are now stubs for some allocation functions, which at least make the analysis sound and don't leave important functions uncalled. Nevertheless, even with symbolic locks we find almost everything to be racing because these net drivers heavily use data and mutexes stored deep in dynamically allocated structs. Our char drivers are much easier because they use global arrays.