Avoid or generalize global counters used in `TmpLabel` and `Block`

[viper-admin]

Created by @fpoli on 2019-01-15 15:09 Last updated on 2019-01-15 15:15

The data races reported in https://github.com/viperproject/silver/issues/256 have been quickly fixed in pull request https://github.com/viperproject/silver/pull/408 by using AtomicIntegers.

The fix works, but several improvements are possible:

• Malte suggested to develop some kind of generic thread-safe counter or symbol generator, usable by both Silicon and Carbon.
• Fábio suggested to use, if it exists, the Scala equivalent of Java's AtomicInteger.
• In my opinion, for the conversion of methods to CFG the global counters can be avoided entirely, by using method-local counters for TmpLabel and Block (allocating a symbol generator in CfgGenerator#methodToCfg, and passing it as an additional parameter in toCfg method calls). This should avoid the overhead of thread-safe counters.

[viper-admin]

@fpoli on 2019-01-15 15:10:

• edited the description

[viper-admin]

@fpoli on 2019-01-15 15:11:

• edited the description

[viper-admin]

@fpoli on 2019-01-15 15:15:

• edited the description