Skip to content

Speed up RebalancingClientsWithStats #2

Open
Open
Speed up RebalancingClientsWithStats#2

Description

@lemmy
lemmy
opened on Aug 24, 2022

With the following Java module override for RebalancingClientsWithStats!IsBalanced, generating 5k traces of depth 1000 takes TLC less than five minutes. With the newly introduced TLCExt!TLCCache wrapping Quantify in AppActiveCount(a), the runtime is down to 6 minutes., Without the module override, TLC takes around 15 minutes.

package tlc2.module;

import tla2sany.semantic.ExprOrOpArgNode;
import tlc2.overrides.Evaluation;
import tlc2.tool.TLCState;
import tlc2.tool.coverage.CostModel;
import tlc2.tool.impl.Tool;
import tlc2.util.Context;
import tlc2.value.impl.BoolValue;
import tlc2.value.impl.FcnRcdValue;
import tlc2.value.impl.IntValue;
import tlc2.value.impl.IntervalValue;
import tlc2.value.impl.SetEnumValue;
import tlc2.value.impl.Value;
import util.UniqueString;

public class RebalancingClientsWithStats {
	
	/*
	    /\ \A q \in queue : active[q] # 0
	    /\ \A a1, a2 \in app : 
	        /\ AppHasSubscriptions(a1)
	        /\ AppHasSubscriptions(a2)
	        /\ AppActiveCount(a1) - AppActiveCount(a2) \in { -1, 0, 1}
	 */
	
	@Evaluation(definition = "IsBalanced", module = "RebalancingClientsWithStats", warn = true, silent = false)
	public static Value IsBalanced(final Tool tool, final ExprOrOpArgNode[] args, final Context c,
			final TLCState s0, final TLCState s1, final int control, final CostModel cm) {
		
		
		// /\ \A q \in queue : active[q] # 0
		final FcnRcdValue active = (FcnRcdValue) s0.lookup(UniqueString.of("active"));
		final IntervalValue queue = (IntervalValue) s0.lookup(UniqueString.of("queue"));
		
		for (int i = 0; i < queue.size(); i++) {
			final Value q = queue.elementAt(i);
			final Value activeQ = active.select(q);
			
			if (activeQ.equals(IntValue.ValZero)) {
				return BoolValue.ValFalse;
			}
		}
		
		
		// /\ \A a1, a2 \in app : 
        // 	/\ app_queues[a1] # {}
        // 	/\ app_queues[a2] # {}
        // 	/\ Quantify(queue, LAMBDA q : active[q] = a1) - Quantify(queue, LAMBDA q : active[q] = a2) \in { -1, 0, 1}
		final IntervalValue app = (IntervalValue) s0.lookup(UniqueString.of("app"));
		final FcnRcdValue appQueues = (FcnRcdValue) s0.lookup(UniqueString.of("app_queues"));

		// /\ \A a1, a2 \in app : 
		for (int i = 0; i < app.size(); i++) {
			final Value a1 = app.elementAt(i);
			
			//   /\ app_queues[a1] # {}
			if (SetEnumValue.EmptySet.equals(appQueues.select(a1))) {
				return BoolValue.ValFalse;
			}
			
			for (int j = i + 1; j < app.size(); j++) {
				final Value a2 = app.elementAt(j);

				//	/\ app_queues[a2] # {}
				if (SetEnumValue.EmptySet.equals(appQueues.select(a2))) {
					return BoolValue.ValFalse;
				}
				
		        // 	Quantify(queue, LAMBDA q : active[q] = a1) - Quantify(queue, LAMBDA q : active[q] = a2) \in { -1, 0, 1}
				// or 
				//  Cardinality({q \in queue : active[q] = a1}) - Cardinality({q \in queue : active[q] = a2}) \in { -1, 0, 1}
				
				int aac1 = 0;
				int aac2 = 0;

				for (int k = 0; k < queue.size(); k++) {
					final Value q = queue.elementAt(k);
					if (active.select(q).equals(a1)) {
						aac1++;
					}
					if (active.select(q).equals(a2)) {
						aac2++;
					}
				}
				
				if (Math.abs(aac1 - aac2) > 1) {
					return BoolValue.ValFalse;
				}
			}
		}
	
		return BoolValue.ValTrue;
	}

}

Module Override:

TLC2 Version 2.18 of Day Month 20??
Warning: Please run the Java VM, which executes TLC with a throughput optimized garbage collector, by passing the "-XX:+UseParallelGC" property.
(Use the -nowarning option to disable this warning.)
Running Random Simulation with seed 42 with 1 worker on 10 cores with 8192MB heap and 64MB offheap memory [pid: 6789] (Mac OS X 12.5.1 x86_64, Azul Systems, Inc. 11.0.14.1 x86_64).
Parsing file /Users/markus/src/TLA/_specs/formal-methods-playground/tla/tlaplus-conf/rabbitmq/RebalancingClientsWithStats.tla
Parsing file /Users/markus/src/TLA/tla/tlatools/org.lamport.tlatools/class/tla2sany/StandardModules/Sequences.tla
Parsing file /Users/markus/src/TLA/tla/tlatools/org.lamport.tlatools/class/tla2sany/StandardModules/Integers.tla
Parsing file /Users/markus/src/TLA/tla/tlatools/org.lamport.tlatools/class/tla2sany/StandardModules/FiniteSets.tla
Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-1198702587823076175/FiniteSetsExt.tla (file:/Users/markus/src/TLA/_specs/CommunityModules/build/modules/FiniteSetsExt.tla)
Parsing file /Users/markus/src/TLA/tla/tlatools/org.lamport.tlatools/class/tla2sany/StandardModules/Naturals.tla
Parsing file /Users/markus/src/TLA/tla/tlatools/org.lamport.tlatools/class/tla2sany/StandardModules/TLC.tla
Parsing file /Users/markus/src/TLA/tla/tlatools/org.lamport.tlatools/class/tla2sany/StandardModules/TLCExt.tla
Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-1198702587823076175/CSV.tla (file:/Users/markus/src/TLA/_specs/CommunityModules/build/modules/CSV.tla)
Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-1198702587823076175/IOUtils.tla (file:/Users/markus/src/TLA/_specs/CommunityModules/build/modules/IOUtils.tla)
Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-1198702587823076175/Functions.tla (file:/Users/markus/src/TLA/_specs/CommunityModules/build/modules/Functions.tla)
Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-1198702587823076175/Folds.tla (file:/Users/markus/src/TLA/_specs/CommunityModules/build/modules/Folds.tla)
Semantic processing of module Naturals
Semantic processing of module Sequences
Semantic processing of module Integers
Semantic processing of module FiniteSets
Semantic processing of module Folds
Semantic processing of module Functions
Semantic processing of module FiniteSetsExt
Semantic processing of module TLC
Semantic processing of module TLCExt
Semantic processing of module CSV
Semantic processing of module IOUtils
Semantic processing of module RebalancingClientsWithStats
Starting... (2022-08-23 16:53:10)
Computed 58 initial states...
Progress: 565917 states checked, 1150 traces generated (trace length: mean=484, var(x)=82088, sd=287)
Progress: 1143448 states checked, 2310 traces generated (trace length: mean=484, var(x)=82738, sd=288)
Progress: 1668861 states checked, 3372 traces generated (trace length: mean=484, var(x)=83361, sd=289)
Progress: 2172265 states checked, 4364 traces generated (trace length: mean=484, var(x)=83426, sd=289)
Progress: 2493819 states checked, 5000 traces generated (trace length: mean=484, var(x)=83761, sd=289)
The number of states generated: 2493819
Simulation using seed 42 and aril 0
Finished in 04min 40s at (2022-08-23 16:57:49)

TLCExt!TLCCache:

TLC2 Version 2.18 of Day Month 20??
Warning: Please run the Java VM, which executes TLC with a throughput optimized garbage collector, by passing the "-XX:+UseParallelGC" property.
(Use the -nowarning option to disable this warning.)
Running Random Simulation with seed 42 with 1 worker on 10 cores with 8192MB heap and 64MB offheap memory [pid: 7528] (Mac OS X 12.5.1 x86_64, Azul Systems, Inc. 11.0.14.1 x86_64).
Parsing file /Users/markus/src/TLA/_specs/formal-methods-playground/tla/tlaplus-conf/rabbitmq/RebalancingClientsWithStats.tla
Parsing file /Users/markus/src/TLA/tla/tlatools/org.lamport.tlatools/class/tla2sany/StandardModules/Sequences.tla
Parsing file /Users/markus/src/TLA/tla/tlatools/org.lamport.tlatools/class/tla2sany/StandardModules/Integers.tla
Parsing file /Users/markus/src/TLA/tla/tlatools/org.lamport.tlatools/class/tla2sany/StandardModules/FiniteSets.tla
Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-5533939031590169833/FiniteSetsExt.tla (file:/Users/markus/src/TLA/_specs/CommunityModules/build/modules/FiniteSetsExt.tla)
Parsing file /Users/markus/src/TLA/tla/tlatools/org.lamport.tlatools/class/tla2sany/StandardModules/Naturals.tla
Parsing file /Users/markus/src/TLA/tla/tlatools/org.lamport.tlatools/class/tla2sany/StandardModules/TLC.tla
Parsing file /Users/markus/src/TLA/tla/tlatools/org.lamport.tlatools/class/tla2sany/StandardModules/TLCExt.tla
Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-5533939031590169833/CSV.tla (file:/Users/markus/src/TLA/_specs/CommunityModules/build/modules/CSV.tla)
Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-5533939031590169833/IOUtils.tla (file:/Users/markus/src/TLA/_specs/CommunityModules/build/modules/IOUtils.tla)
Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-5533939031590169833/Functions.tla (file:/Users/markus/src/TLA/_specs/CommunityModules/build/modules/Functions.tla)
Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-5533939031590169833/Folds.tla (file:/Users/markus/src/TLA/_specs/CommunityModules/build/modules/Folds.tla)
Semantic processing of module Naturals
Semantic processing of module Sequences
Semantic processing of module Integers
Semantic processing of module FiniteSets
Semantic processing of module Folds
Semantic processing of module Functions
Semantic processing of module FiniteSetsExt
Semantic processing of module TLC
Semantic processing of module TLCExt
Semantic processing of module CSV
Semantic processing of module IOUtils
Semantic processing of module RebalancingClientsWithStats
Starting... (2022-08-23 17:20:05)
Computed 58 initial states...
Progress: 394195 states checked, 804 traces generated (trace length: mean=484, var(x)=80620, sd=284)
Progress: 798094 states checked, 1614 traces generated (trace length: mean=484, var(x)=82862, sd=288)
Progress: 1214987 states checked, 2456 traces generated (trace length: mean=484, var(x)=83627, sd=289)
Progress: 1631646 states checked, 3297 traces generated (trace length: mean=484, var(x)=83475, sd=289)
Progress: 2051725 states checked, 4130 traces generated (trace length: mean=484, var(x)=83566, sd=289)
Progress: 2466603 states checked, 4934 traces generated (trace length: mean=484, var(x)=84004, sd=290)
Progress: 2493819 states checked, 5000 traces generated (trace length: mean=484, var(x)=83761, sd=289)
The number of states generated: 2493819
Simulation using seed 42 and aril 0
Finished in 06min 05s at (2022-08-23 17:26:09)

Baseline (original spec):

TLC2 Version 2.18 of Day Month 20??
Warning: Please run the Java VM, which executes TLC with a throughput optimized garbage collector, by passing the "-XX:+UseParallelGC" property.
(Use the -nowarning option to disable this warning.)
Running Random Simulation with seed 42 with 1 worker on 10 cores with 8192MB heap and 64MB offheap memory [pid: 6902] (Mac OS X 12.5.1 x86_64, Azul Systems, Inc. 11.0.14.1 x86_64).
Parsing file /Users/markus/src/TLA/_specs/formal-methods-playground/tla/tlaplus-conf/rabbitmq/RebalancingClientsWithStats.tla
Parsing file /Users/markus/src/TLA/tla/tlatools/org.lamport.tlatools/class/tla2sany/StandardModules/Sequences.tla
Parsing file /Users/markus/src/TLA/tla/tlatools/org.lamport.tlatools/class/tla2sany/StandardModules/Integers.tla
Parsing file /Users/markus/src/TLA/tla/tlatools/org.lamport.tlatools/class/tla2sany/StandardModules/FiniteSets.tla
Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-7923786008999413418/FiniteSetsExt.tla (file:/Users/markus/src/TLA/_specs/CommunityModules/build/modules/FiniteSetsExt.tla)
Parsing file /Users/markus/src/TLA/tla/tlatools/org.lamport.tlatools/class/tla2sany/StandardModules/Naturals.tla
Parsing file /Users/markus/src/TLA/tla/tlatools/org.lamport.tlatools/class/tla2sany/StandardModules/TLC.tla
Parsing file /Users/markus/src/TLA/tla/tlatools/org.lamport.tlatools/class/tla2sany/StandardModules/TLCExt.tla
Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-7923786008999413418/CSV.tla (file:/Users/markus/src/TLA/_specs/CommunityModules/build/modules/CSV.tla)
Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-7923786008999413418/IOUtils.tla (file:/Users/markus/src/TLA/_specs/CommunityModules/build/modules/IOUtils.tla)
Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-7923786008999413418/Functions.tla (file:/Users/markus/src/TLA/_specs/CommunityModules/build/modules/Functions.tla)
Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-7923786008999413418/Folds.tla (file:/Users/markus/src/TLA/_specs/CommunityModules/build/modules/Folds.tla)
Semantic processing of module Naturals
Semantic processing of module Sequences
Semantic processing of module Integers
Semantic processing of module FiniteSets
Semantic processing of module Folds
Semantic processing of module Functions
Semantic processing of module FiniteSetsExt
Semantic processing of module TLC
Semantic processing of module TLCExt
Semantic processing of module CSV
Semantic processing of module IOUtils
Semantic processing of module RebalancingClientsWithStats
Starting... (2022-08-23 17:03:06)
Computed 58 initial states...
Progress: 157951 states checked, 329 traces generated (trace length: mean=476, var(x)=81713, sd=286)
Progress: 328938 states checked, 678 traces generated (trace length: mean=484, var(x)=79546, sd=282)
Progress: 485109 states checked, 983 traces generated (trace length: mean=484, var(x)=81422, sd=285)
Progress: 646415 states checked, 1311 traces generated (trace length: mean=484, var(x)=83380, sd=289)
Progress: 810842 states checked, 1642 traces generated (trace length: mean=484, var(x)=82721, sd=288)
Progress: 970229 states checked, 1959 traces generated (trace length: mean=484, var(x)=83782, sd=289)
Progress: 1138908 states checked, 2300 traces generated (trace length: mean=484, var(x)=82878, sd=288)
Progress: 1295656 states checked, 2622 traces generated (trace length: mean=484, var(x)=83530, sd=289)
Progress: 1467501 states checked, 2971 traces generated (trace length: mean=484, var(x)=83728, sd=289)
Progress: 1623112 states checked, 3282 traces generated (trace length: mean=484, var(x)=83317, sd=289)
Progress: 1780569 states checked, 3590 traces generated (trace length: mean=484, var(x)=83582, sd=289)
Progress: 1950557 states checked, 3933 traces generated (trace length: mean=484, var(x)=83776, sd=289)
Progress: 2121930 states checked, 4266 traces generated (trace length: mean=484, var(x)=83364, sd=289)
Progress: 2280531 states checked, 4571 traces generated (trace length: mean=484, var(x)=83542, sd=289)
Progress: 2442111 states checked, 4880 traces generated (trace length: mean=484, var(x)=83893, sd=290)
Progress: 2493819 states checked, 5000 traces generated (trace length: mean=484, var(x)=83761, sd=289)
The number of states generated: 2493819
Simulation using seed 42 and aril 0
Finished in 15min 18s at (2022-08-23 17:18:23)

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions