From a8c79270b350827f80b87a3a1a914a0a983cd502 Mon Sep 17 00:00:00 2001 From: jjenista Date: Fri, 16 Oct 2009 17:59:16 +0000 Subject: [PATCH] working on directto benchmark--removing code like unused constructors that hinder program understanding, and tinkering with the stripped down version for exploring analysis weaknesses --- Robust/src/Benchmarks/mlp/directto/README.txt | 64 ++++++++++++++++++- .../Benchmarks/mlp/directto/mlp-java/D2.java | 12 ++-- .../mlp/directto/mlp-java/FlightList.java | 6 -- .../mlp/directto/mlp-java/Message.java | 6 -- .../Benchmarks/mlp/directto/mlp-java/makefile | 2 +- .../directto/mlp-small-for-testing/D2.java | 50 ++++++--------- .../mlp-small-for-testing/Flight.java | 2 +- .../mlp-small-for-testing/FlightList.java | 8 +-- .../mlp-small-for-testing/Message.java | 37 +++++------ .../mlp-small-for-testing/MessageList.java | 5 +- .../TrajectorySynthesizer.java | 5 +- .../directto/mlp-small-for-testing/makefile | 19 ++++-- 12 files changed, 128 insertions(+), 88 deletions(-) diff --git a/Robust/src/Benchmarks/mlp/directto/README.txt b/Robust/src/Benchmarks/mlp/directto/README.txt index 3bc08bec..79c28d6c 100644 --- a/Robust/src/Benchmarks/mlp/directto/README.txt +++ b/Robust/src/Benchmarks/mlp/directto/README.txt @@ -1,3 +1,63 @@ -The DirectTo benchmark reads in a text file to build a list of -messages for tracking and routing aircraft without conflicts. +Any statement *** in asterix *** is an assertion that +disjoint reachability analysis should be able to verify. +The DirectTo benchmark executes a list of messages from +an input file to solve a safe aircraft routing problem. + +The D2 (direct-to) singleton object has a singleton +reference to: + -ReadWrite, reads input file, creates messages + -MessageList, commands to execute for building problem + -Static, structure of static constants from input file + -AircraftList, all types of aircraft in problem + -FlightList, list of flights in algorithm + -FixList, list of fixes algorithm computes + -Algorithm, reads from Static + -TrajectorySynthesizer, reads from Static + -Flight, why a singleton Flight object? +so: +*** all memory in the program should be reachable from +at most one of any singleton (D2, Static, etc) *** + +MessageList has a Vector of Message objects, where each +one specifys an effect for other structures such as +setting a constant in the Static singleton, or adding +an aircraft type to the Aircraft list, etc. Message +objects themselves only have references that are freshly +allocated, so: +*** Message objects should be disjoint *** + +The ReadWrite singleton appends new Message objects +to the MessageList and has no references of its own, +*** Nothing is reachable from a ReadWrite *** + +The Static singleton has primitive members, so +*** Nothing is reachable from a Static *** + +AircraftList has a Vector of Aircraft objects, where +each one has a String for type and some primitive +attributes, where the type is generated from a +StringTokenizer (getting a token gets a new String), +and in practice is disjoint for every Aircraft, so: +*** Aircraft objects should be disjoint *** + +FixList has a Vector of Fix objects, where each one +has a String name and a Point2d (an alternate point +in a flight plan?). I believe they are not modified +after being built from freshly allocated tokenizing, +*** Fix objects should be disjoint *** + +FlightList has a Vector of Flight objects which have +several fresh, set-once references (flightID String, +a Track, etc). +Flight objects may share Aircraft (types), + + + +In Message.executeMessage(), if you comment out every +message handler except any one of these, they cause +Message objects to show sharing: + - FlightList.addFlightPlan() + - FlightList.amendFlightInfo() + - FlightList.amendFlightPlan() (still a quick analysis!) + - FlightList.sendingAircraft() diff --git a/Robust/src/Benchmarks/mlp/directto/mlp-java/D2.java b/Robust/src/Benchmarks/mlp/directto/mlp-java/D2.java index 477e9d34..ae30bed3 100755 --- a/Robust/src/Benchmarks/mlp/directto/mlp-java/D2.java +++ b/Robust/src/Benchmarks/mlp/directto/mlp-java/D2.java @@ -7,24 +7,22 @@ public class D2 { public ReadWrite singletonReadWrite ; public ReadWrite getReadWrite () { return singletonReadWrite ; } + public MessageList singletonMessageList ; public MessageList getMessageList () { return singletonMessageList ; } public Static singletonStatic ; public Static getStatic () { return singletonStatic ; } public AircraftList singletonAircraftList ; public AircraftList getAircraftList () { return singletonAircraftList ; } - public Algorithm singletonAlgorithm ; public Algorithm getAlgorithm () { return singletonAlgorithm ; } - public FixList singletonFixList ; public FixList getFixList () { return singletonFixList ; } - public Flight singletonFlight ; public Flight getFlight () { return singletonFlight ; } public FlightList singletonFlightList ; public FlightList getFlightList () { return singletonFlightList ; } - public MessageList singletonMessageList ; public MessageList getMessageList () { return singletonMessageList ; } + public FixList singletonFixList ; public FixList getFixList () { return singletonFixList ; } + public Algorithm singletonAlgorithm ; public Algorithm getAlgorithm () { return singletonAlgorithm ; } public TrajectorySynthesizer singletonTrajectorySynthesizer; public TrajectorySynthesizer getTrajectorySynthesizer() { return singletonTrajectorySynthesizer; } public D2() { singletonReadWrite = new ReadWrite (); + singletonMessageList = new MessageList (); singletonStatic = new Static (); singletonAircraftList = new AircraftList (); + singletonFlightList = new FlightList (); singletonFixList = new FixList (); singletonAlgorithm = new Algorithm (); - singletonFlight = new Flight (""); - singletonFlightList = new FlightList (); - singletonMessageList = new MessageList (); singletonTrajectorySynthesizer = new TrajectorySynthesizer(); } diff --git a/Robust/src/Benchmarks/mlp/directto/mlp-java/FlightList.java b/Robust/src/Benchmarks/mlp/directto/mlp-java/FlightList.java index d0cd5dce..9167b75e 100755 --- a/Robust/src/Benchmarks/mlp/directto/mlp-java/FlightList.java +++ b/Robust/src/Benchmarks/mlp/directto/mlp-java/FlightList.java @@ -11,12 +11,6 @@ public class FlightList { f=new Vector(100); } - /* - public void addFlight(int index, Flight flight) { - f.addElement(index,flight); - } - */ - public void addFlightPlan(D2 d2, int time, StringTokenizer st) { Flight newFlight=disjoint flightAdd new Flight(st.nextToken()); noFlights++; diff --git a/Robust/src/Benchmarks/mlp/directto/mlp-java/Message.java b/Robust/src/Benchmarks/mlp/directto/mlp-java/Message.java index 08c7e4f6..f83a2e3c 100755 --- a/Robust/src/Benchmarks/mlp/directto/mlp-java/Message.java +++ b/Robust/src/Benchmarks/mlp/directto/mlp-java/Message.java @@ -11,12 +11,6 @@ public class Message { this.parameters=parameters; } - public Message(Message m) { - this.time=m.time; - this.type=m.type; - this.parameters=m.parameters; - } - public void executeMessage(D2 d2) { System.out.println("Executing message of type "+type); diff --git a/Robust/src/Benchmarks/mlp/directto/mlp-java/makefile b/Robust/src/Benchmarks/mlp/directto/mlp-java/makefile index 6892efc2..df0027f9 100644 --- a/Robust/src/Benchmarks/mlp/directto/mlp-java/makefile +++ b/Robust/src/Benchmarks/mlp/directto/mlp-java/makefile @@ -4,7 +4,7 @@ PROGRAM=test SOURCE_FILES=D2.java #smalltest.java BUILDSCRIPT=~/research/Robust/src/buildscript -BSFLAGS= -debug -nooptimize -mainclass $(MAIN_CLASS) -justanalyze -ownership -ownallocdepth 1 -ownwritedots final -ownaliasfile aliases.txt -enable-assertions +BSFLAGS= -debug -nooptimize -mainclass $(MAIN_CLASS) #-justanalyze -ownership -ownallocdepth 1 -ownwritedots final -ownaliasfile aliases.txt -enable-assertions all: $(PROGRAM).bin diff --git a/Robust/src/Benchmarks/mlp/directto/mlp-small-for-testing/D2.java b/Robust/src/Benchmarks/mlp/directto/mlp-small-for-testing/D2.java index 5a0c06f9..6ebd0b5b 100644 --- a/Robust/src/Benchmarks/mlp/directto/mlp-small-for-testing/D2.java +++ b/Robust/src/Benchmarks/mlp/directto/mlp-small-for-testing/D2.java @@ -5,54 +5,44 @@ //import java.io.*; public class D2 { - public ReadWrite rw; - private Static singletonStatic ; public Static getStatic () { return singletonStatic ; } - private AircraftList singletonAircraftList ; public AircraftList getAircraftList () { return singletonAircraftList ; } - private Algorithm singletonAlgorithm ; public Algorithm getAlgorithm () { return singletonAlgorithm ; } - private FixList singletonFixList ; public FixList getFixList () { return singletonFixList ; } - private Flight singletonFlight ; public Flight getFlight () { return singletonFlight ; } - private FlightList singletonFlightList ; public FlightList getFlightList () { return singletonFlightList ; } - private MessageList singletonMessageList ; public MessageList getMessageList () { return singletonMessageList ; } - private TrajectorySynthesizer singletonTrajectorySynthesizer; public TrajectorySynthesizer getTrajectorySynthesizer() { return singletonTrajectorySynthesizer; } + public ReadWrite singletonReadWrite ; public ReadWrite getReadWrite () { return singletonReadWrite ; } + public MessageList singletonMessageList ; public MessageList getMessageList () { return singletonMessageList ; } + public Static singletonStatic ; public Static getStatic () { return singletonStatic ; } + public AircraftList singletonAircraftList ; public AircraftList getAircraftList () { return singletonAircraftList ; } + public FlightList singletonFlightList ; public FlightList getFlightList () { return singletonFlightList ; } + public FixList singletonFixList ; public FixList getFixList () { return singletonFixList ; } + public Algorithm singletonAlgorithm ; public Algorithm getAlgorithm () { return singletonAlgorithm ; } + public TrajectorySynthesizer singletonTrajectorySynthesizer; public TrajectorySynthesizer getTrajectorySynthesizer() { return singletonTrajectorySynthesizer; } public D2() { + singletonReadWrite = new ReadWrite (); + singletonMessageList = new MessageList (); singletonStatic = new Static (); singletonAircraftList = new AircraftList (); + singletonFlightList = new FlightList (); singletonFixList = new FixList (); singletonAlgorithm = new Algorithm (); - singletonFlight = new Flight ( "" ); - singletonFlightList = new FlightList (); - singletonMessageList = new MessageList (); - singletonTrajectorySynthesizer = new TrajectorySynthesizer(); + singletonTrajectorySynthesizer = new TrajectorySynthesizer(); } public static void main(String arg[]) { System.out.println("D2 - Application started"); D2 d2 = new D2(); - - - d2.rw=new ReadWrite(); - d2.rw.read(d2); - + d2.getReadWrite().read(d2); + d2.getMessageList().executeAll(d2); - int count = 0; + /* while( d2.getFlightList().anyPlanesAlive() ) { - // d2.getAlgorithm().doIteration(d2); - - count++; - if( count % 10000 == 0 ) { - //System.out.println( "iteration "+count ); - } - - if( count == 1000 ) { - break; - } + d2.getAlgorithm().doIteration(d2); } - d2.rw.write(d2); + d2.getReadWrite().write(d2); + */ + + System.out.println("D2 - Application finished"); } } diff --git a/Robust/src/Benchmarks/mlp/directto/mlp-small-for-testing/Flight.java b/Robust/src/Benchmarks/mlp/directto/mlp-small-for-testing/Flight.java index b5bae9c5..baad640c 100644 --- a/Robust/src/Benchmarks/mlp/directto/mlp-small-for-testing/Flight.java +++ b/Robust/src/Benchmarks/mlp/directto/mlp-small-for-testing/Flight.java @@ -48,7 +48,7 @@ public class Flight /*implements Cloneable*/ { } public static Flight copyOf(Flight f) { - Flight fNew = disjoint flightCopy new Flight(f.flightID); + Flight fNew = /*disjoint flightCopy*/ new Flight(f.flightID); fNew.trialStatus = f.trialStatus; fNew.aircraftType = f.aircraftType; fNew.track = f.track; diff --git a/Robust/src/Benchmarks/mlp/directto/mlp-small-for-testing/FlightList.java b/Robust/src/Benchmarks/mlp/directto/mlp-small-for-testing/FlightList.java index d0cd5dce..1d9a500a 100644 --- a/Robust/src/Benchmarks/mlp/directto/mlp-small-for-testing/FlightList.java +++ b/Robust/src/Benchmarks/mlp/directto/mlp-small-for-testing/FlightList.java @@ -11,14 +11,8 @@ public class FlightList { f=new Vector(100); } - /* - public void addFlight(int index, Flight flight) { - f.addElement(index,flight); - } - */ - public void addFlightPlan(D2 d2, int time, StringTokenizer st) { - Flight newFlight=disjoint flightAdd new Flight(st.nextToken()); + Flight newFlight=/*disjoint flightAdd*/ new Flight(st.nextToken()); noFlights++; f.addElement(newFlight); diff --git a/Robust/src/Benchmarks/mlp/directto/mlp-small-for-testing/Message.java b/Robust/src/Benchmarks/mlp/directto/mlp-small-for-testing/Message.java index f002f4a5..30542b69 100644 --- a/Robust/src/Benchmarks/mlp/directto/mlp-small-for-testing/Message.java +++ b/Robust/src/Benchmarks/mlp/directto/mlp-small-for-testing/Message.java @@ -11,17 +11,11 @@ public class Message { this.parameters=parameters; } - public Message(Message m) { - this.time=m.time; - this.type=m.type; - this.parameters=m.parameters; - } - public void executeMessage(D2 d2) { System.out.println("Executing message of type "+type); + //static messages /* - //static messages if (type.compareTo("SET_MAP_SIZE")==0) { System.out.println("Setting the map size..."); d2.getStatic().setMapSize(parameters); @@ -45,37 +39,44 @@ public class Message { else if (type.compareTo("REMOVE_FIX")==0) { System.out.println("Removing a fix..."); d2.getFixList().removeFix(parameters); - } - else*/ if (type.compareTo("ADD_AIRCRAFT")==0) { + } + else if (type.compareTo("ADD_AIRCRAFT")==0) { System.out.println("Adding an aircraft..."); d2.getAircraftList().addAircraft(parameters); - } else - /* + } else if (type.compareTo("REMOVE_AIRCRAFT")==0) { System.out.println("Removing an aircraft..."); d2.getAircraftList().removeAircraft(parameters); } - //dynamic messages + */ + + //dynamic messages + /* if (type.compareTo("DO_WORK")==0) d2.getAlgorithm().setInitialTime(time); */ + + /* if (type.compareTo("ADD_FLIGHT_PLAN")==0) { System.out.println("Adding flight plan..."); d2.getFlightList().addFlightPlan(d2,time,parameters); } - /* - else if (type.compareTo("REMOVE_FLIGHT_PLAN")==0) { + */ + + + /*else if (type.compareTo("REMOVE_FLIGHT_PLAN")==0) { System.out.println("Removing flight plan..."); d2.getFlightList().removeFlightPlan(time,parameters); - } + } else if (type.compareTo("AMEND_FLIGHT_INFO")==0) { System.out.println("Amending flight info..."); d2.getFlightList().amendFlightInfo(d2, time,parameters); - } - else if (type.compareTo("AMEND_FLIGHT_PLAN")==0) { + } + else*/ if (type.compareTo("AMEND_FLIGHT_PLAN")==0) { System.out.println("Amending flight plan..."); d2.getFlightList().amendFlightPlan(d2, time,parameters); - } + } + /* else if (type.compareTo("SENDING_AIRCRAFT")==0) { System.out.println("Sending aircraft data..."); d2.getFlightList().sendingAircraft(d2, time,parameters); diff --git a/Robust/src/Benchmarks/mlp/directto/mlp-small-for-testing/MessageList.java b/Robust/src/Benchmarks/mlp/directto/mlp-small-for-testing/MessageList.java index c91db3bb..2f268cb4 100644 --- a/Robust/src/Benchmarks/mlp/directto/mlp-small-for-testing/MessageList.java +++ b/Robust/src/Benchmarks/mlp/directto/mlp-small-for-testing/MessageList.java @@ -10,12 +10,13 @@ public class MessageList { public Message data() { Message m = (Message) messages.elementAt(0); - messages.removeElementAt(0); return m; } public Message next() { - return data(); + Message m = (Message) messages.elementAt(0); + messages.removeElementAt(0); + return m; } public boolean hasNext() { diff --git a/Robust/src/Benchmarks/mlp/directto/mlp-small-for-testing/TrajectorySynthesizer.java b/Robust/src/Benchmarks/mlp/directto/mlp-small-for-testing/TrajectorySynthesizer.java index 5de6652b..bec9ff85 100644 --- a/Robust/src/Benchmarks/mlp/directto/mlp-small-for-testing/TrajectorySynthesizer.java +++ b/Robust/src/Benchmarks/mlp/directto/mlp-small-for-testing/TrajectorySynthesizer.java @@ -30,8 +30,7 @@ public class TrajectorySynthesizer { } public /*static*/ Trajectory updateTrajectory (D2 d2, double time, Flight flight) { - return null; - /* System.out.println("Updating trajectory for "+flight.flightID); + System.out.println("Updating trajectory for "+flight.flightID); int i; setInitialParameters(flight); System.out.println("Starting position: "+currentPos); @@ -62,7 +61,7 @@ public class TrajectorySynthesizer { flight.traject=traject; System.out.println("Finished updating trajectory ..."); - return traject;*/ + return traject; } private /*static*/ void setInitialParameters(Flight flight) { diff --git a/Robust/src/Benchmarks/mlp/directto/mlp-small-for-testing/makefile b/Robust/src/Benchmarks/mlp/directto/mlp-small-for-testing/makefile index 6892efc2..bf80219e 100644 --- a/Robust/src/Benchmarks/mlp/directto/mlp-small-for-testing/makefile +++ b/Robust/src/Benchmarks/mlp/directto/mlp-small-for-testing/makefile @@ -1,12 +1,18 @@ -MAIN_CLASS=D2 #smalltest +MAIN_CLASS=D2 PROGRAM=test -SOURCE_FILES=D2.java #smalltest.java +SOURCE_FILES=D2.java BUILDSCRIPT=~/research/Robust/src/buildscript -BSFLAGS= -debug -nooptimize -mainclass $(MAIN_CLASS) -justanalyze -ownership -ownallocdepth 1 -ownwritedots final -ownaliasfile aliases.txt -enable-assertions +BSFLAGS= -debug -nooptimize -mainclass $(MAIN_CLASS) -all: $(PROGRAM).bin +#DBCALLFLAGS= -owndebugcaller main -owndebugcallee executeAll +DBCALLFLAGS= -owndebugcaller executeAll -owndebugcallee executeMessage -owndebugcallcount 1 +#DBCALLFLAGS= -owndebugcaller executeMessage -owndebugcallee amendFlightPlan + +ANALYZEFLAGS= -justanalyze $(DBCALLFLAGS) -ownership -ownallocdepth 1 -ownwritedots final -ownaliasfile aliases.txt -enable-assertions + +all: $(PROGRAM) view: PNGs eog *.png & @@ -16,9 +22,12 @@ PNGs: DOTs DOTs: $(PROGRAM).bin -$(PROGRAM).bin: $(SOURCE_FILES) +$(PROGRAM): $(SOURCE_FILES) $(BUILDSCRIPT) $(BSFLAGS) -o $(PROGRAM) $(SOURCE_FILES) +analyze: $(SOURCE_FILES) + $(BUILDSCRIPT) $(BSFLAGS) $(ANALYZEFLAGS) -o $(PROGRAM) $(SOURCE_FILES) + clean: rm -f $(PROGRAM).bin rm -fr tmpbuilddirectory -- 2.34.1