experimenting with directto benchmark

diff --git a/Robust/src/Benchmarks/mlp/directto/README.txt b/Robust/src/Benchmarks/mlp/directto/README.txt
index 79c28d6c2a74638fc418e4ab10ae86a3b03b7e5c..25e5404db6bfe2c444e37ef812f18e1a43c2dc5f 100644 (file)
--- 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 90e5a74248e72f7afe0ddd5d5d43d46f381e3a65..df975538cbc457cb4c2d5bd1c962e98260a9d3b7 100755 (executable)
--- 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 32e712b5cc904992c443ae2df0dff3247ba303b6..f3d570e4dba39ebe3c8b61dfdb68fda591ed88b6 100755 (executable)
--- 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 ae30bed3821eb3732006499638fd1012de58b2d9..3d9381ea8635242d800a58e44d88db66f01b410d 100755 (executable)
--- 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 b2b3e7379394370049c9113a6828a3bb9d30eb78..9e1d6e90558501955ea7d071878f49199202bf5b 100755 (executable)
--- 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 b5bae9c52700a030c3b1810798ced48c072810ec..baad640cf1168a3888b84461344f79f62b88177e 100755 (executable)
--- 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 9167b75ecadd2c0ba6dfaa145a3b8f24e2b87835..1d9a500aa2b1334e598c950365a5f9d330a6bb07 100755 (executable)
--- 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 2f268cb414a4ff7dc2008aa3e53f0f4c39a511f2..d8f5063eeaf8607d25bb31503b3cef91246c0338 100755 (executable)
--- 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 746516ec3a872f9be7a80cd561e1becb46b0a9cb..2311acb2897e86e155cff2de6a6c36e00524b0e7 100644 (file)
--- 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<rAux.noFixes;i++)
     //  rAux.addFix(d2,i,st.nextToken());      
-    //////////////////////////////
-    rAux.addFix(d2,0,st.nextToken());      
-
+    //////////////////////////////    
+    rAux.addFix(d2,0,st.nextToken());         
 
     fAux.fPlan.setRoute(rAux);
-    fAux.fPlan.setCruiseParam(Double.parseDouble(st.nextToken()), Double.parseDouble(st.nextToken()));
+    //fAux.fPlan.setCruiseParam(Double.parseDouble(st.nextToken()), Double.parseDouble(st.nextToken()));
   }
 
     public  void amendFlightInfo(D2 d2, int time, StringTokenizer st) {

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 43a226ef3ee834642276d1fabccfd96d589e09fa..23bc7746dc308b047e6f8e018afd82f8a136c38d 100644 (file)
--- a/Robust/src/Benchmarks/mlp/directto/mlp-small-for-testing/makefile
+++ b/Robust/src/Benchmarks/mlp/directto/mlp-small-for-testing/makefile
@@ -6,19 +6,28 @@ SOURCE_FILES=D2.java
 BUILDSCRIPT=~/research/Robust/src/buildscript
 BSFLAGS= -debug -mainclass $(MAIN_CLASS) -joptimize -flatirusermethods #-flatirlibmethods
 
-#DBCALLFLAGS= -owndebugcaller main -owndebugcallee executeAll 
+##########################################################
+## For inspecting a particularly problematic call chain
+##########################################################
+DBCALLFLAGS= -owndebugcaller main -owndebugcallee executeAll 
 #DBCALLFLAGS= -owndebugcaller executeAll -owndebugcallee executeMessage -owndebugcallcount 0
-#DBCALLFLAGS= -owndebugcaller executeAll -owndebugcallee next -owndebugcallcount 0
-#DBCALLFLAGS= -owndebugcaller executeAll -owndebugcallee hasNext -owndebugcallcount 0
-#DBCALLFLAGS= -owndebugcaller executeAll -owndebugcallee size -owndebugcallcount 0
-#DBCALLFLAGS= -owndebugcaller executeMessage -owndebugcallee getFlightList -owndebugcallcount 0
 #DBCALLFLAGS= -owndebugcaller executeMessage -owndebugcallee amendFlightPlan -owndebugcallcount 0
-#DBCALLFLAGS= -owndebugcaller amendFlightPlan -owndebugcallee getFlight -owndebugcallcount 0
+#DBCALLFLAGS= -owndebugcaller amendFlightPlan -owndebugcallee setRoute -owndebugcallcount 0
+
+
 #DBCALLFLAGS= -owndebugcaller amendFlightPlan -owndebugcallee addFix -owndebugcallcount 0
 #DBCALLFLAGS= -owndebugcaller addFix -owndebugcallee addFix -owndebugcallcount 0
 #DBCALLFLAGS= -owndebugcaller addFix -owndebugcallee insertElementAt -owndebugcallcount 0
 #DBCALLFLAGS= -owndebugcaller insertElementAt -owndebugcallee ensureCapacity -owndebugcallcount 0
 
+
+#DBCALLFLAGS= -owndebugcaller executeMessage -owndebugcallee getFlightList -owndebugcallcount 0
+#DBCALLFLAGS= -owndebugcaller amendFlightPlan -owndebugcallee getFlight -owndebugcallcount 0
+#DBCALLFLAGS= -owndebugcaller executeAll -owndebugcallee next -owndebugcallcount 0
+#DBCALLFLAGS= -owndebugcaller executeAll -owndebugcallee hasNext -owndebugcallcount 0
+#DBCALLFLAGS= -owndebugcaller executeAll -owndebugcallee size -owndebugcallcount 0
+
+
 ANALYZEFLAGS= -justanalyze $(DBCALLFLAGS) -ownership -ownallocdepth 1 -ownwritedots final -ownaliasfile aliases.txt -enable-assertions
 
 all: $(PROGRAM)