-- | This file contains a semantic interpreter designed in continuation passing style -- | and implemented in Haskell. It implements the operational semantics of -- | the concurrent language Lsyn^omega presented in section 3.1 of the paper: -- | -- | "Abstractness of Metric Semantics for Concurrency in Continuation-Passing Style" -- | Authors: Eneia Nicolae Todoran and Gabriel Ciobanu -- | Submitted to ACM Coputing Surveys (2025) -- | -- | The language Lsyn^omega is essentially based on well-known Milner's CCS [1]. -- | The language Lsyn^omega extends the (uniform) language with synchronization -- | described in [2] (section 11.2) with the joint input construct of -- | process calculus CCS^n presented in [3]. -- | -- | [1] R. Milner, Communication and Concurrency, Prentice Hall, 1989. -- | [2] J.W. de Bakker and E.P. de Vink, Control Flow Semantics, MIT Press, 1996. -- | [3] C. Laneve and A. Vitale, "The expressive power of synchronizations", Proc. of LICS 2010, pp. 382-–391, 2010. -- | -- | In CCS^n calculus the joint input construct is a list of names of length at most n. -- | Unlike CCS^n, in the language Lsyn^omega a joint input is a non-empty multiset -- | (implemented as a Haskell list) that can contain a (finite, but) arbitrarily large number of names. -- | The language Lsyn^omega provides support for synchronous multiparty interactions -- | between an arbitrarily large (finite) number of concurrent processes. -- | -- | Function 'osem' implements the operational semantics of the concurrent language Lsyn^omega. -- | -- | In the experiments given below, s1, s2, s3 and s4 implement the Lsyn^omega statements -- | introduced in Example 2 in our paper submitted to ACM Computing Surveys. -- | -- | The semantic interpreter can be tested as in the following examples: -- | -- | Main> run s1 -- | ... -- | Main> run s2 -- | ... -- | Main> run s3 -- | ... -- | Main> run s4 -- | ... -- | (Main> is the GHC prompt) -- | -- | The same experiments can be performed using function 'main': -- | -- | -- | Main> main -- | ... -- | -- | Further Lsyn^omega example programs (which are not presented in the paper) -- | can be tested using function 'main2' -- | -- | -- | Main> main2 -- | ... -- | -- | Remark: In this implementation we avoided using various specific Haskell -- | library functions. Had we have done this, the implementation would have been shorter -- | but the connection with our ACM Computing Surveys submission would have been -- | less obvious to a non Haskell-expert reader -- | Syntax of Lsyn^omega type Name = String -- ^ Names type CoName = String -- ^ Co-names type J = [Name] -- ^ Joint inputs type B = String data IAct = Tau | B B deriving Eq -- ^ Internal actions data Act = I IAct | S CoName | J J | Stop -- ^ Actions deriving Eq type Yvar = String -- ^ Recursion variables (procedure variables) -- | Statements and declarations data Stat = Act Act -- ^ Actions | Y Yvar -- ^ Recursion variable | New Stat Name -- ^ Restriction | Seq Stat Stat -- ^ Sequential composition | Ned Stat Stat -- ^ Nondeterministic choice | Par Stat Stat -- ^ Parallel composition (merge) | Lpar Stat Stat -- ^ Left merge | Syn Stat Stat -- ^ Synchronization merge | Lsyn Stat Stat -- ^ Left synchronization merge deriving Eq type Decl = Yvar -> Stat -- ^ Declarations -- | Interaction multisets type U = [M] data M = ActM Act | NewM Name U -- | Interaction function iu :: U -> [Act] iu ([ActM act]) = [act] iu ([NewM c u]) = case iu u of [I b] -> [I b] [J j] -> if not (c `elem` j) then [J j] else [Stop] w -> if (out w) && (not (c `elem` (compl w))) then w else [Stop] iu u = chi (bigsumms [ iu [m] | m <- u ]) out :: [Act] -> Bool out w = and [ pout act | act <- w ] where pout :: Act -> Bool pout (S c) = True pout _ = False compl :: [Act] -> J compl w = [ c | S c <- w ] chi :: [Act] -> [Act] chi w = let wia = [ I b | I b <- w ] win = [ J j | J j <- w ] wout = [ S c | S c <- w ] wstop = [ Stop | Stop <- w ] in case (wia,wstop,win) of ([],[],[J j]) -> if j `eqms` (compl wout) then [I Tau] else if wout == [] then [J j] else if (compl wout) `subms` j then [J (j `diffms` (compl wout))] else [Stop] ([],[],[]) -> if wout /= [] then wout else [Stop] _ -> [Stop] -- | Asynchronous resumptions data K = Ke | Ks Stat -- | Nameless abstractions and sequences of statements data F = Fz ZExp | Lambda F deriving Eq data ZExp = Zi Int | Za Act | Znew ZExp Name | Zseq ZExp Stat | Zlpar ZExp Stat | Zlsyn ZExp ZExp deriving Eq type X = [Stat] -- | Synchronous resumptions and configurations type Res = (X,F) data Conf = Conf Stat Res | E deriving Eq -- | Transition relation designed in continuation-passing style tss :: Decl -> Conf -> [(IAct,Conf)] tss decl E = [] tss decl (Conf (Act a) ([],f)) = let Fz z = eval f (Za a) (u,k) = evz z w = iu u in case (w,k) of ([I b],Ke) -> [(b,E)] ([I b],Ks s) -> [(b,Conf s ([],Lambda (Fz (Zi 0))))] _ -> [] tss decl (Conf (Act a) (s:x,f)) = tss decl (Conf s (x,eval f (Za a))) tss decl (Conf (Y y) (x,f)) = tss decl (Conf (decl y) (x,f)) tss decl (Conf (New s ch) (x,f)) = tss decl (Conf s (x,Lambda (eval f (Znew ( Zi 0) ch)))) tss decl (Conf (Ned s1 s2) (x,f)) = tss decl (Conf s1 (x,f)) `union` tss decl (Conf s2 (x,f)) tss decl (Conf (Seq s1 s2) (x,f)) = tss decl (Conf s1 (x,Lambda (eval f (Zseq (Zi 0) s2)))) tss decl (Conf (Lpar s1 s2) (x,f)) = tss decl (Conf s1 (x,Lambda (eval f (Zlpar (Zi 0) s2)))) tss decl (Conf (Lsyn s1 s2) (x,f)) = tss decl (Conf s1 (s2:x,Lambda (Lambda (eval f (Zlsyn (Zi 1) (Zi 0)))))) tss decl (Conf (Syn s1 s2) (x,f)) = tss decl (Conf s1 (s2:x,Lambda (Lambda (eval f (Zlsyn (Zi 1) (Zi 0)))))) `union` tss decl (Conf s2 (s1:x,Lambda (Lambda (eval f (Zlsyn (Zi 1) (Zi 0)))))) tss decl (Conf (Par s1 s2) (x,f)) = tss decl (Conf s1 (x,Lambda (eval f (Zlpar (Zi 0) s2)))) `union` tss decl (Conf s2 (x,Lambda (eval f (Zlpar (Zi 0) s1)))) `union` tss decl (Conf s1 (s2:x,Lambda (Lambda (eval f (Zlsyn (Zi 1) (Zi 0)))))) `union` tss decl (Conf s2 (s1:x,Lambda (Lambda (eval f (Zlsyn (Zi 1) (Zi 0)))))) -- | Final semantic domain type P = [Q] data Q = Epsilon | Delta | Q IAct Q deriving Eq prefix :: IAct -> P -> P prefix b p = [ Q b q | q <- p ] -- | Operational semantics bigphi :: Decl -> (Conf -> P) -> (Conf -> P) bigphi decl semo E = [Epsilon] bigphi decl semo t = case tss decl t of [] -> [Delta] ts -> bigunion [ prefix b (semo t') | (b,t') <- ts ] os :: Conf -> P os = fix (bigphi decl) osem :: Stat -> P osem s = os (Conf s ([],Lambda (Fz (Zi 0)))) -- | Operations on nameless (De Bruijn) terms of type F eval :: F -> ZExp -> F eval (Lambda f) z1 = shiftF (-1) (substF 0 (shiftZ 1 z1) f) substF :: Int -> ZExp -> F -> F substF i z (Lambda f) = Lambda (substF (i+1) (shiftZ 1 z) f) substF i z (Fz z1) = Fz (substZ i z z1) where substZ :: Int -> ZExp -> ZExp -> ZExp substZ i z (Zi i0) = if i==i0 then z else Zi i0 substZ i z (Za a) = Za a substZ i z (Znew z1 c) = Znew (substZ i z z1) c substZ i z (Zseq z1 x) = Zseq (substZ i z z1) x substZ i z (Zlpar z1 x) = Zlpar (substZ i z z1) x substZ i z (Zlsyn z1 z2) = Zlsyn (substZ i z z1) (substZ i z z2) shiftF :: Int -> F -> F shiftF d f = shiftFaux d 0 f shiftFaux :: Int -> Int -> F -> F shiftFaux d h (Lambda f) = (Lambda (shiftFaux d (h+1) f)) shiftFaux d h (Fz z) = Fz (shiftZaux d h z) shiftZ :: Int -> ZExp -> ZExp shiftZ d z = shiftZaux d 0 z shiftZaux :: Int -> Int -> ZExp -> ZExp shiftZaux d h (Zi i) = if i (U,K) evz (Zi i) = error "evz: defined only for expressions without free variables" evz (Za a) = ([ActM a],Ke) evz (Znew e c) = case evz e of (u,Ke) -> ([NewM c u],Ke) (u,Ks s) -> ([NewM c u],Ks (New s c)) evz (Zseq e s2) = case evz e of (u,Ke) -> (u,Ks s2) (u,Ks s) -> (u,Ks (Seq s s2)) evz (Zlpar e s2) = case evz e of (u,Ke) -> (u,Ks s2) (u,Ks s) -> (u,Ks (Par s s2)) evz (Zlsyn e1 e2) = case (evz e1,evz e2) of ((u1,Ke),(u2,Ke)) -> (u1 `summs` u2,Ke) ((u1,Ks s1),(u2,Ke)) -> (u1 `summs` u2,Ks s1) ((u1,Ke),(u2,Ks s2)) -> (u1 `summs` u2,Ks s2) ((u1,Ks s1),(u2,Ks s2)) -> (u1 `summs` u2,Ks (Par s1 s2)) -- | Fixed point operator fix :: (a -> a) -> a fix f = f (fix f) -- | Multiset operations summs :: [a] -> [a] -> [a] summs u1 u2 = u1 ++ u2 bigsumms :: [[a]] -> [a] bigsumms [] = [] bigsumms (u:us) = u `summs` (bigsumms us) subms :: Eq a => [a] -> [a] -> Bool subms [] [] = True subms [] _ = True subms _ [] = False subms (x:xs) xs' = if (x `elem` xs') then subms xs (remove x xs') else False eqms :: Eq a => [a] -> [a] -> Bool eqms [] [] = True eqms [] _ = False eqms _ [] = False eqms (x:xs) xs' = if (x `elem` xs') then eqms xs (remove x xs') else False diffms :: Eq a => [a] -> [a] -> [a] diffms xs [] = xs diffms xs (x':xs') = if (elem x' xs) then diffms (remove x' xs) xs' else diffms xs xs' remove :: Eq a => a -> [a] -> [a] remove x [] = [] remove x (x':xs) = if (x == x') then xs else x' : remove x xs -- | Set operations union :: Eq a => [a] -> [a] -> [a] union [] ys = ys union (x : xs) ys = if x `elem` ys then union xs ys else x : union xs ys bigunion :: Eq a => [[a]] -> [a] bigunion [] = [] bigunion (xs:xss) = xs `union` (bigunion xss) -- | Show instances instance Show IAct where show Tau = "tau" show (B b) = b instance Show Q where show Epsilon = "\n[]" show Delta = "\n[deadlock]" show (Q b q) = "\n[" ++ (aux (Q b q)) ++ "]" where aux (Q b Epsilon) = show b aux (Q b Delta) = show b ++ ",deadlock" aux (Q b q) = show b ++ "," ++ aux q -- | Test support function run :: Stat -> P run s = osem s ------------------------------------------------------------------------------------------- ------------------------------------ Test examples ---------------------------------------- ------------------------------------------------------------------------------------------- -- | Function 'main' runs the Lsyn^omega programs introduced in the paper in Example 2. main = do { print (run s1); print (run s2); print (run s3); print (run s4) } s1, s2, s3, s4 :: Stat s1 = Par (Act (I (B "b1"))) (Act (I (B "b2"))) s2 = Par (Act (J ["c0"])) (Act (S "c0")) s3 = Lsyn (New (Lsyn (Act (J ["c1","c2"])) (Act (S "c1"))) "c1") (Act (S "c2")) s4 = Syn (New (Syn (Act (J ["c1","c2"])) (Act (S "c1"))) "c1") (Act (S "c2")) -- | Function 'main2' can be used to run Lsyn^omega programs which are not presented in the paper. -- | Statement s5 is similar to statement s4, but uses the operator for parallel composition (merge) -- | instead of the synchronization merge operator. Statement s6 is a sequential composition -- | between statement s1 and the internal action b3. Statements s7, s8 and s9 are more complex. -- | Statement s7 specifies a multiparty synchronous interaction between 4 (=3+1) concurrent processes. -- | Statements s8 and s9 extend statement s7 with operations for sequential composition -- | and procedure calls. main2 = do { print (run s5); print (run s6); print (run s7); print (run s8); print (run s9) } s5, s6, s7, s8 :: Stat s5 = Par (New (Par (Act (J ["c1","c2"])) (Act (S "c1"))) "c1") (Act (S "c2")) s6 = Seq (Par (Act (I (B "b1"))) (Act (I (B "b2")))) (Act (I (B "b3"))) s7 = Par (New (Par (New (Par (Act (J ["c1","c2","c3"])) (Act (S "c1"))) "c1") (Act (S "c2"))) "c2") (Act (S "c3")) s8 = Seq (Par (New (Par (New (Par (Act (J ["c1","c2","c3"])) (Act (S "c1"))) "c1") (Act (S "c2"))) "c2") (Seq (Act (I (B "b1"))) (Act (S "c3")))) (Y "y8") s9 = Seq (Y "y9") (Par (New (Par (New (Par (Act (J ["c1","c2","c3"])) (Act (S "c1"))) "c1") (Act (S "c2"))) "c2") (Seq (Act (S "c3")) (Act (I (B "b3"))))) decl :: Decl decl "y8" = Ned (Act (I (B "b2"))) (Act (I (B "b3"))) decl "y9" = Ned (Act (I (B "b1"))) (Act (I (B "b2")))