From: jjenista Date: Fri, 6 Nov 2009 22:48:38 +0000 (+0000) Subject: experimenting with directto benchmark X-Git-Url: http://plrg.eecs.uci.edu/git/?a=commitdiff_plain;h=6fc7c3b5d739276899207deaac9abc1c43ddb9a7;p=IRC.git experimenting with directto benchmark --- diff --git a/Robust/src/Benchmarks/mlp/directto/README.txt b/Robust/src/Benchmarks/mlp/directto/README.txt index 79c28d6c..25e5404d 100644 --- a/Robust/src/Benchmarks/mlp/directto/README.txt +++ b/Robust/src/Benchmarks/mlp/directto/README.txt @@ -4,6 +4,7 @@ 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 @@ -19,6 +20,7 @@ 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 @@ -26,32 +28,42 @@ an aircraft type to the Aircraft list, etc. Message objects themselves only have references that are freshly allocated, so: *** Message objects should be disjoint *** +ANALYSIS FALSELY REPORTS SHARING + 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 *** +*** Aircraft objects should be disjoint *** +VERIFIED BY ANALYSIS + 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 *** +ANALYSIS FALSELY REPORTS SHARING + 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), +*** Flight objects may share Aircraft (types) *** +VERIFIED BY ANALYSIS +...and other objects also. In Message.executeMessage(), if you comment out every diff --git a/Robust/src/Benchmarks/mlp/directto/mlp-java/AircraftList.java b/Robust/src/Benchmarks/mlp/directto/mlp-java/AircraftList.java index 90e5a742..df975538 100755 --- a/Robust/src/Benchmarks/mlp/directto/mlp-java/AircraftList.java +++ b/Robust/src/Benchmarks/mlp/directto/mlp-java/AircraftList.java @@ -13,7 +13,7 @@ public class AircraftList { // sets the parameters of the aircraft number "pos": its name, its lift and its thrust public void setAircraft(String name,double lift,double thrust) { - aircrafts.addElement(new Aircraft(name,lift,thrust)); + aircrafts.addElement(/*disjoint aircraft*/ new Aircraft(name,lift,thrust)); } public Aircraft getAircraft(String name) { diff --git a/Robust/src/Benchmarks/mlp/directto/mlp-java/Algorithm.java b/Robust/src/Benchmarks/mlp/directto/mlp-java/Algorithm.java index 32e712b5..f3d570e4 100755 --- a/Robust/src/Benchmarks/mlp/directto/mlp-java/Algorithm.java +++ b/Robust/src/Benchmarks/mlp/directto/mlp-java/Algorithm.java @@ -28,7 +28,7 @@ public class Algorithm { return false; } - public /*static*/ Point4d findConflict(D2 d2, Flight a, Flight b) { + public /*static*/ Point4d findConflict(D2 d2, Flight a, Flight b) { Point4d conflictPoint=new Point4d(Point4d.outOfRangeTime(),0,0,0); if (a.flightID!=b.flightID) { Vector p1=a.traject.p; diff --git a/Robust/src/Benchmarks/mlp/directto/mlp-java/D2.java b/Robust/src/Benchmarks/mlp/directto/mlp-java/D2.java index ae30bed3..3d9381ea 100755 --- a/Robust/src/Benchmarks/mlp/directto/mlp-java/D2.java +++ b/Robust/src/Benchmarks/mlp/directto/mlp-java/D2.java @@ -16,14 +16,14 @@ public class D2 { 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 (); - singletonTrajectorySynthesizer = new TrajectorySynthesizer(); + singletonReadWrite = disjoint rw new ReadWrite (); + singletonMessageList = disjoint ml new MessageList (); + singletonStatic = disjoint st new Static (); + singletonAircraftList = disjoint al new AircraftList (); + singletonFlightList = disjoint fl new FlightList (); + singletonFixList = disjoint xl new FixList (); + singletonAlgorithm = disjoint ag new Algorithm (); + singletonTrajectorySynthesizer = disjoint ts new TrajectorySynthesizer(); } public static void main(String arg[]) { diff --git a/Robust/src/Benchmarks/mlp/directto/mlp-java/FixList.java b/Robust/src/Benchmarks/mlp/directto/mlp-java/FixList.java index b2b3e737..9e1d6e90 100755 --- a/Robust/src/Benchmarks/mlp/directto/mlp-java/FixList.java +++ b/Robust/src/Benchmarks/mlp/directto/mlp-java/FixList.java @@ -21,7 +21,7 @@ public class FixList { // and its coordinates public /*static*/ void setFix(String name,float x,float y) { - _fixes.addElement(new Fix(name,(Point2d) new Point2d(x,y))); + _fixes.addElement(/* disjoint fix */ new Fix(name,(Point2d) new Point2d(x,y))); } public /*static*/ String getFix(int index) diff --git a/Robust/src/Benchmarks/mlp/directto/mlp-java/Flight.java b/Robust/src/Benchmarks/mlp/directto/mlp-java/Flight.java index b5bae9c5..baad640c 100755 --- a/Robust/src/Benchmarks/mlp/directto/mlp-java/Flight.java +++ b/Robust/src/Benchmarks/mlp/directto/mlp-java/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-java/FlightList.java b/Robust/src/Benchmarks/mlp/directto/mlp-java/FlightList.java index 9167b75e..1d9a500a 100755 --- a/Robust/src/Benchmarks/mlp/directto/mlp-java/FlightList.java +++ b/Robust/src/Benchmarks/mlp/directto/mlp-java/FlightList.java @@ -12,7 +12,7 @@ public class FlightList { } 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-java/MessageList.java b/Robust/src/Benchmarks/mlp/directto/mlp-java/MessageList.java index 2f268cb4..d8f5063e 100755 --- a/Robust/src/Benchmarks/mlp/directto/mlp-java/MessageList.java +++ b/Robust/src/Benchmarks/mlp/directto/mlp-java/MessageList.java @@ -37,7 +37,7 @@ public class MessageList { StringTokenizer st=new StringTokenizer(line); int time=Integer.parseInt(st.nextToken()); String type=st.nextToken(); - Message newMessage=disjoint msgs new Message(time,type,st); + Message newMessage=/*disjoint msgs*/ new Message(time,type,st); messages.addElement(newMessage); if (type.equals("DO_WORK")) return true; 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 746516ec..2311acb2 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 @@ -43,12 +43,11 @@ public class FlightList { // do this once //for (int i=0;i