[Haskell][Isabelle] Improving performance

[diekmann]

Over the last releases, the performance both of the Isabelle tests and the Haskell tool declined. My guess: this is related to the upcoming support of IPv6. In general, since we support IP addresses as machine words of arbitrary (but fixed) length, performance declined.

It would be interested to profile and inspect the generated Haskell code in detail. I guess there are also many performance issues nor related to the machine word implementation. Next, hot sports with poorly performing of inefficient code need to be tuned. Of course, we want to prove that the new and efficient code computes exactly the same things as the old code. Isabelle, here we come :-)

This feature can also be implemented as part of a thesis or interdisciplinary project at Technische Universität München.

[diekmann]

COST CENTRE          MODULE                     %time %alloc

divmod_integer       Network.IPTables.Generated  18.6   32.2
times_int            Network.IPTables.Generated  12.9   15.1
minus_nat            Network.IPTables.Generated  12.4   23.7
power                Network.IPTables.Generated   9.3   12.2
sgn_integer          Network.IPTables.Generated   5.4    0.0
equal_nat            Network.IPTables.Generated   5.0    0.0
max                  Network.IPTables.Generated   4.0    0.0
mod_integer          Network.IPTables.Generated   3.4    0.0
equal_int            Network.IPTables.Generated   2.6    0.0
divide_integer       Network.IPTables.Generated   2.6    0.0
plus_int             Network.IPTables.Generated   2.5    1.6
bitAND_int           Network.IPTables.Generated   2.4    1.1
divmod_integer.(...) Network.IPTables.Generated   2.2    6.4
apsnd                Network.IPTables.Generated   1.7    1.9
divmod_integer.\     Network.IPTables.Generated   1.5    0.0
mod_int              Network.IPTables.Generated   1.3    0.3
funpow               Network.IPTables.Generated   0.9    1.3

[diekmann]

There is too much noise in the match expressions. Just look at all those (MatchAnd MatchAny (MatchAnd MatchAny ...

https://github.com/diekmann/Iptables_Semantics/blob/refactoring/thy/Iptables_Semantics/Primitive_Matchers/Protocols_Normalize.thy#L510