working on #20 #18 #5 #4

marcelosousa · Jan 5, 2017 · f22d33c · f22d33c
1 parent 5592d3a
commit f22d33c
Show file tree

Hide file tree

Showing 9 changed files with 362 additions and 688 deletions.
diff --git a/benchmarks/basic/ai/basic.c b/benchmarks/basic/ai/basic.c
@@ -3,23 +3,22 @@
 int x = 0;
 
 void *p(void* arg){
-  x = x + 1;
+  int y = 1;
 }
 
 
 int main(){
   /* references to the threads */
-  pthread_t p_t;
-  pthread_t q_t;
+  pthread_t p_t[2];
 
   /* create the threads and execute */
-  pthread_create(&p_t, NULL, p, NULL);
-  pthread_create(&q_t, NULL, p, NULL);
+  pthread_create(&p_t[0], NULL, p, NULL);
+  pthread_create(&p_t[1], NULL, p, NULL);
 
   /* wait for the threads to finish */
-  pthread_join(&p_t, NULL);
-  pthread_join(&q_t, NULL);
-  
+  pthread_join(&p_t[1], NULL);
+  pthread_join(&p_t[0], NULL);
+
   return 0;
 }
 
diff --git a/src/Domain/Action.hs b/src/Domain/Action.hs
@@ -9,52 +9,56 @@
 module Domain.Action where
 
 import Language.SimpleC.AST
+import Domain.MemAddr
 import Domain.Util
 import Model.GCS
 
 -- Default implementation of an
 -- Action using read write sets
 -- over the memory addresses 
 -- accessed.
-data Act
+data Act v
   = Act
-  { rds     :: MemAddrs -- read
-  , wrs     :: MemAddrs -- write
-  , locks   :: MemAddrs -- locks
-  , unlocks :: MemAddrs -- unlocks
-  , tcreate :: MemAddrs -- phtread_create 
-  , tjoin   :: MemAddrs -- phtread_join
-  , texit   :: MemAddrs -- phtread_exit
+  { rds     :: MemAddrs v -- read
+  , wrs     :: MemAddrs v -- write
+  , locks   :: MemAddrs v -- locks
+  , unlocks :: MemAddrs v -- unlocks
+  , tcreate :: MemAddrs v -- phtread_create 
+  , tjoin   :: MemAddrs v -- phtread_join
+  , texit   :: MemAddrs v -- phtread_exit
   }
   deriving (Eq,Ord)
 
-instance Show Act where
+instance Show v => Show (Act v) where
   show (Act r w l u c j e) = 
     "Act { r = " ++ show r ++ ", w = " ++ show w ++ ", lk = " ++ show l ++ ", ulk = " ++ show u ++ ", c = " ++ show c ++ ", j = " ++ show j ++ ", e = " ++ show e
 
-bot_act :: Act
+bot_act :: Act v
 bot_act =
   Act bot_maddrs bot_maddrs bot_maddrs bot_maddrs bot_maddrs bot_maddrs bot_maddrs
 
-read_act :: SymId -> Scope -> Act
-read_act sym scope = Act (MemAddrs [MemAddr sym scope]) bot_maddrs bot_maddrs bot_maddrs bot_maddrs bot_maddrs bot_maddrs
+read_act :: SymId -> v -> Scope -> Act v
+read_act sym offset scope = Act (MemAddrs [MemAddr sym offset scope]) bot_maddrs bot_maddrs bot_maddrs bot_maddrs bot_maddrs bot_maddrs
 
-write_act :: SymId -> Scope -> Act
-write_act sym scope = Act bot_maddrs (MemAddrs [MemAddr sym scope]) bot_maddrs bot_maddrs bot_maddrs bot_maddrs bot_maddrs
+write_act :: SymId -> v -> Scope -> Act v
+write_act sym offset scope = Act bot_maddrs (MemAddrs [MemAddr sym offset scope]) bot_maddrs bot_maddrs bot_maddrs bot_maddrs bot_maddrs
 
-create_thread_act :: SymId -> Act
-create_thread_act tid = 
-  Act bot_maddrs bot_maddrs bot_maddrs bot_maddrs (MemAddrs [MemAddr tid Global]) bot_maddrs bot_maddrs
+write_act_addr :: MemAddrs v -> Act v
+write_act_addr addr = Act bot_maddrs addr bot_maddrs bot_maddrs bot_maddrs bot_maddrs bot_maddrs
 
-join_thread_act :: SymId -> Act
-join_thread_act tid = 
-  Act bot_maddrs bot_maddrs bot_maddrs bot_maddrs bot_maddrs (MemAddrs [MemAddr tid Global]) bot_maddrs 
+create_thread_act :: SymId -> v -> Act v
+create_thread_act tid offset = 
+  Act bot_maddrs bot_maddrs bot_maddrs bot_maddrs (MemAddrs [MemAddr tid offset Global]) bot_maddrs bot_maddrs
 
-exit_thread_act :: SymId -> Act
-exit_thread_act tid = 
-  Act bot_maddrs bot_maddrs bot_maddrs bot_maddrs bot_maddrs bot_maddrs (MemAddrs [MemAddr tid Global]) 
+join_thread_act :: SymId -> v -> Act v
+join_thread_act tid offset = 
+  Act bot_maddrs bot_maddrs bot_maddrs bot_maddrs bot_maddrs (MemAddrs [MemAddr tid offset Global]) bot_maddrs 
+
+exit_thread_act :: SymId -> v -> Act v
+exit_thread_act tid offset = 
+  Act bot_maddrs bot_maddrs bot_maddrs bot_maddrs bot_maddrs bot_maddrs (MemAddrs [MemAddr tid offset Global]) 
 
-join_act :: Act -> Act -> Act
+join_act :: Eq v => Act v -> Act v -> Act v
 join_act a1 a2 =
   let r = rds a1 `join_maddrs` rds a2 
       w = wrs a1 `join_maddrs` wrs a2 
@@ -65,22 +69,12 @@ join_act a1 a2 =
       e = texit a1 `join_maddrs` texit a2
   in Act r w l u c j e 
 
-add_writes :: MemAddrs -> Act -> Act
+add_writes :: Eq v => MemAddrs v -> Act v -> Act v
 add_writes ws act@Act{..} =
   let wrs' = ws `join_maddrs` wrs
   in act { wrs = wrs' }
 
-{-
-instance Show Act where
-  show act@Act{..} =
-    let rs = "reads: " ++ show rds
-        wrds = "writes: " ++ show wrs
-        lks = "locks: " ++ show locks
-        ulks = "unlocks: " ++ show unlocks
-    in rs++"\n"++wrds++"\n"++lks++"\n"++ulks
--}
-
-instance Action Act where
+instance Eq v => Action (Act v) where
   isBlocking act@Act{..} = 
     not (is_maddrs_bot locks && is_maddrs_bot unlocks)
   isJoin act@Act{..} = 
@@ -111,14 +105,11 @@ instance Action Act where
   isCreateOf tid_sym a1@Act{..} =
     case tcreate of
       MemAddrTop -> True
-      MemAddrs at -> any (\a -> a == MemAddr tid_sym Global) at 
-
-is_global :: MemAddrs -> Bool
-is_global maddr = case maddr of
-  MemAddrTop -> True
-  MemAddrs l -> any (\a@MemAddr{..} -> level == Global) l
+      MemAddrs at -> any (\a -> case a of 
+         MemAddr tid_sym _ Global -> True
+         _ -> False) at 
 
-act_addrs :: Act -> MemAddrs
+act_addrs :: Eq v => Act v -> MemAddrs v
 act_addrs a@Act{..} =
   rds `join_maddrs` wrs `join_maddrs` locks `join_maddrs` 
   unlocks `join_maddrs` tcreate `join_maddrs` tjoin  `join_maddrs` texit
diff --git a/src/Domain/Interval/Collapse.hs b/src/Domain/Interval/Collapse.hs
@@ -1,4 +1,6 @@
 {-# LANGUAGE RecordWildCards #-}
+{-# LANGUAGE TypeSynonymInstances #-}
+{-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 -------------------------------------------------------------------------------
 -- Module    :  Domain.Interval.Collapse
@@ -16,6 +18,7 @@ import Domain.Action
 import Domain.Interval.Converter
 import Domain.Interval.State
 import Domain.Interval.Value
+import Domain.Interval.API
 import Domain.Util
 import Language.SimpleC.AST
 import Language.SimpleC.Converter (get_symbol_name)
@@ -26,12 +29,12 @@ import qualified Data.Map as M
 import qualified Data.Set as S
 import qualified Debug.Trace as T
 
-type IntGraph = Graph SymId () (IntState,Act) 
-type IntGraphs = Graphs SymId () (IntState,Act)
+type IntGraph = Graph SymId () (IntState,IntAct) 
+type IntGraphs = Graphs SymId () (IntState,IntAct)
 type WItem = (NodeId,EdgeId,NodeId)
 type Worklist = [WItem]
-type ResultList = [(IntState,Pos,Act)]
-type NodeTable = Map NodeId [(IntState,Act)]
+type ResultList = [(IntState,Pos,IntAct)]
+type NodeTable = Map NodeId [(IntState,IntAct)]
 
 data FixState =
   FixState
@@ -52,16 +55,17 @@ showResultList l = "Data Flow Information:\n" ++ (snd $ foldr (\(s,p,a) (n,r) ->
        s_r = s_a ++ show s
    in (n+1, s_r ++ r))  (1,"") l)
 
-is_locked :: System IntState Act -> SExpression -> IntState -> Bool
-is_locked syst expr st = 
-  let lk_ident = get_expr_id expr 
-  in case M.lookup lk_ident (heap st) of
-       Nothing -> error $ "is_locked fatal: cant find info for lock " ++ show lk_ident
-       Just (MCell _ val) -> case val of
-         IntVal [VInt i] -> i == 1  
-         _ -> error $ "is_locked fatal: lock has unsupported values " ++ show val 
+is_locked :: IntState -> Scope -> SExpression -> Bool
+is_locked st scope expr = 
+  let lk_addrs = get_addrs st scope expr 
+  in case read_memory st lk_addrs of
+    []    -> error $ "is_locked fatal: cant find info for lock " ++ show expr
+    [val] -> case val of 
+      IntVal [VInt i] -> i == 1  
+      _ -> error $ "is_locked fatal: lock has unsupported values " ++ show val 
+    l -> error $ "is_locked fatal: lock has unsupported values " ++ show l 
 
-is_live :: TId -> System IntState Act -> EdgeId -> IntGraph -> IntState -> Bool
+is_live :: TId -> System IntState IntAct -> EdgeId -> IntGraph -> IntState -> Bool
 is_live tid syst eId cfg st = 
   let EdgeInfo tags code = get_edge_info cfg eId 
   in case code of
@@ -70,12 +74,13 @@ is_live tid syst eId cfg st =
         "pthread_join" ->
           let tid' = get_tid_expr (Local tid) st (args!!0) 
           in not $ is_enabled syst st tid' 
-        "pthread_mutex_lock" -> not $ is_locked syst (args!!0) st 
+         -- assume the mutex is declared globally 
+        "pthread_mutex_lock" -> not $ is_locked st Global (args!!0)
         _ -> True 
       _ -> True
     _ -> True
 
-instance Collapsible IntState Act where
+instance Collapsible IntState IntAct where
   is_enabled syst st tid =
     let control = controlPart st
         tid_cfg_sym = toThCFGSym st tid
@@ -129,7 +134,7 @@ up_pc i@IntTState{..} t p =
   let st' = update_pc st t p
   in i {st = st'} 
 
-handle_mark :: WItem -> FixOp (IntState,Pos,Act)
+handle_mark :: WItem -> FixOp (IntState,Pos,IntAct)
 handle_mark (pre,eId,post) = do
   fs@FixState{..} <- get
   let node_st = case get_node_info fs_cfg pre of
@@ -157,7 +162,7 @@ handle_mark (pre,eId,post) = do
   case M.lookup post $ node_table cfg' of
     Just [(res_st,res_act)] -> do
       let rwlst = map (\(a,b) -> (post,a,b)) $ succs fs_cfg post
-          e_act = exit_thread_act $ SymId fs_tid
+          e_act = exit_thread_act (SymId fs_tid) zero
       if (Exit `elem` edge_tags) || null rwlst
       then return (res_st,post,res_act `join_act` e_act)
       else return (res_st,post,res_act)
@@ -216,7 +221,7 @@ worklist _wlist = mtrace ("worklist: " ++ show _wlist) $ do
         let nwlist = if is_fix then wlist else (wlist ++ rwlst)
         worklist nwlist
 
-join_update :: NodeTable -> NodeId -> (IntState, Act) -> (Bool, NodeTable)
+join_update :: NodeTable -> NodeId -> (IntState, IntAct) -> (Bool, NodeTable)
 join_update node_table node (st,act) =
   case M.lookup node node_table of
     Nothing -> (False, M.insert node [(st,act)] node_table)
@@ -230,7 +235,7 @@ join_update node_table node (st,act) =
            else (False, M.insert node [(nst,nact)] node_table)
       _ -> error "join_update: more than one state in the list"
 
-strong_update :: NodeTable -> NodeId -> (IntState,Act) -> (Bool, NodeTable)
+strong_update :: NodeTable -> NodeId -> (IntState,IntAct) -> (Bool, NodeTable)
 strong_update node_table node (st,act) =
   case M.lookup node node_table of
     Nothing -> (False, M.insert node [(st,act)] node_table)