IEICETRANS.??,VOL.Exx–??,NO.xxXXXX200x 1 LETTER A Concurrent Model for Imperative Languages with Improved Atomicity Keehang KWON†, Member and Daeseong KANG††, Nonmember 7 1 0 SUMMARY Weproposeanewconcurrentmodelforimper- treats ♯(G1,...,Gn) atomic. This can be easily imple- 2 ativelanguageswhereconcurrencyoccursatasubprogramlevel. mentedbydesigningourinterpreterworkingintwodif- n This model introduces a new block sequential statement of the ferentmodes: theconcurrentmodeandthetraditional a form♯(G1,...,Gn)whereeachGiisastatement. Thisstatement sequential mode. Thus, if our interpreter encounters J tellsthemachinetoexecute G1,...,Gn sequentiallyandatomi- cally(i.e.,withoutinterleaving). Itthereforeenhancesatomicity ♯(G1,...,Gn), it switches from the concurrent mode 7 andpredictabilityinconcurrentprogramming. to the sequential mode and proceeds just like the tra- WeillustrateourideaviaCk,anextensionofthecorecon- ditional C interpreter. In this way, atomicity of this ] currentCwiththenewblocksequential statement. L statement is guaranteed. We intend to use this con- keywords: concurrency,imperativelanguages,blocksequential. P struct to each critical region. . This paper focuses on the minimum core of C, en- s 1. Introduction c hancedwithconcurrencyatasubprogramlevel. Thisis [ topresenttheideaasconciselyaspossible. Theremain- 1 Adding concurrency to imperative programming – C, der of this paper is structured as follows. We describe v itsextension[6]andJava–isanattractivetask. While Ck,anextensionofconcurrentCwithanewstatement 5 concurrent programming may appear to be a simple in Section 2. In Section 3, we present an example of 8 task,ithasproventoodifficulttouse,predictordebug. Ck. Section 4 concludes the paper. 7 An analysis shows that this difficulty comes from 1 the fact that interleavings among threads – which are 2. The Language 0 typically done by OS schedulers – are quite arbitrary . 1 and cannot be controlled at all by the programmer. The language is core C with procedure definitions. It 0 We observe that concurrent programming can be is describedby G- andD-formulasgivenby the syntax 7 made easier by making interleaving less arbitrary and rules below: 1 more controlled. Inspired by [4],[5], we propose two : v ideas for this. First, we propose a concurrent model G::= true|A|x=E |;(G1,...,Gn)| Xi withitsownembeddedscheduler. Ourschedulerworks ♯(G1,...,Gn) D ::= A=G |∀x D on a high-level: it allows the execution to switch from r a oneassigmentstatementtoanother. Thisisincontrast to OS schedulers which allows the execution to switch In the above, A represents a head of an atomic fromonemachineinstructiontoanother. Forexample, procedure definition of the form p(x1,...,xn) where the assignment statement c = c+1 is atomic in the x1,...,xn are parameters. A D-formula is called a sense that it runs to completion without being inter- procedure definition. In the transition system to be leaved. This reduces nondeterminism and error known considered,aG-formulawillfunctionasathreadanda as transient errors. setofG-formulas(i.e.,asetofthreads)willfunctionas Second, semaphores and monitors are typically the main statement, and a set of D-formulas enhanced used as facilities for mutual exclusion. We propose with the machine state (a set of variable-value bind- a simpler method to solve mutual exclusion. Toward ings) will constitute a program. Thus, a program is a this end, we propose a new block sequential state- union of two disjoint sets, i.e., {D1,...,Dn}∪θ where ment ♯(G1,...,Gn), where each Gi is a statement. each Di is a D-formula and θ represents the machine This has the following execution semantics: execute state. Note that θ is initially set to an empty set and G1,...,Gn sequentially and consecutively (i.e., with- will be updated dynamically during execution via the out being interleaved). In other words, our interpreter assignment statements. Wewillpresentaninterpreterforourlanguagevia Manuscript received January 1, 2003. a proof theory [3],[7]–[9]. This is in contrast to other Manuscript revised January 1, 2003. complex approaches to describing an interpreter for Final manuscript received January 1, 2003. †The authors are with Computer Eng., DongA Univer- concurrent languages [1],[2]. Note that our interpreter sity. email:[email protected] alternatesbetweenthe concurrentexecutionphaseand ††TheauthoriswithElectronicsEng.,DongAUniversity. the backchaining phase. In the concurrent execution IEICETRANS.??,VOL.Exx–??,NO.xxXXXX200x 2 phase (denoted by ex(P,k(Γ,G,∆),P′)) it tries to se- ex(P,k(Γ,∆),P )). % an empty sequential com- 1 lect and execute a thread G among a set of threads position is a success. (Γ,G,∆) with respect to a program P and produce a newprogramP′byreducingGtosimplerformsuntilG (8) ex(P,k(Γ,;(G1,...,Gm),∆),P2) ← (ex(P,k(G ),P ) seqand becomes an assignment statement, true or a procedure 1 1 call. Therules(4)-(11)dealwiththisphase. Hereboth ex(P1,k(Γ,;(G2,...,Gm),∆),P2)). % Γand∆denoteasetofG-formulas. IfGbecomesapro- %Ifasequentialcomposition;(G1,...,Gm)ischo- cedurecall,theinterpreterswitchestothebackchaining sen,executeG insequentialmodeandthenreturn 1 mode. Thisisencodedintherule(3). Inthebackchain- to the interpreter with the rest. ing mode (denoted by bc(D,P,A,P′,Γ,∆)), the inter- preter tries to solve a procedure call A and produce a (9) ex(P,k(Γ,repeat(G),∆),P2) ← new program P′ by first reducing a procedure defini- (ex(P,k(G),P1) seqand tionD inaprogramP toitsinstance(viarule(2))and ex(P1,k(Γ,repeat(G),∆),P2)). then backchaining on the resulting definition (via rule % If a repeat statement repeat(G) is chosen, exe- (1)). To be specific, the rule (2) basically deals with cute G in sequential mode and then return to the argument passing: it eliminates the universal quanti- interpreter with the rest plus repeat(G). fier x in ∀xD by picking a value t for x so that the resulting instantiation, written as [t/x]D, matches the (10) ex(P,k(♯()),P). procedure call A. The notation S seqand R denotes % An empty block sequential statement is a suc- the sequential execution of two tasks. To be precise, cess. it denotes the following: execute S and execute R se- quentially. It is considereda success if both executions (11) ex(P,k(Γ,♯(G1,...,Gm),∆),P3) ← (ex(P,k(G ),P ) seqand succeed. Similarly, the notation S parand R denotes 1 1 the parallel execution of two tasks. To be precise, it (ex(P1,k(♯(G2,...,Gm)),P2) seqand ex(P ,k(Γ,∆),P )). denotes the following: execute S and execute R in any 2 3 order. Thus,theexecutionorderisnotimportanthere. %Ifablocksequentialstatement♯(G1,...,Gm)is It is considered a success if both executions succeed. chosen, execute G in sequential mode and then 1 The notation S ← R denotes reverse implication, i.e., ♯(G2,...,Gm) in sequential mode andthen return R→S. to the interpreter (which proceeds in concurrent mode) with the remaining. Definition 1. Let k(G1,...,Gn) be a sequence of threads to run concurrently and let P be a pro- gram. Thenthe notionofexecutinghP,k(G1,...,Gn)i concurrently and producing a new program P′– If ex(P,G,P1) has no derivation, then the interpreter ex(P,k(G1,...,Gn),P′) – is defined as follows: returns the failure. Initially it works in the concur- rent mode. In the concurrent mode, we assume that (1) bc((A=G1),P,A,P1,Γ,∆) ← our interpreter chooses a thread using some predeter- ex(P,k(Γ,G1,∆),P1). % A matching procedure mined algorithm. Note that executing one thread G for A is found. concurrently,denotedbyk(G),isidenticaltoexecuting G sequentially. (2) bc(∀xD,P,A,P ,Γ,∆) ← 1 bc([t/x]D,P,A,P ,Γ,∆). % argument passing 1 3. Examples (3) ex(P,k(Γ,A,∆),P ) ← (D ∈ P parand 1 As a well-knownexample, we examine the system that bc(D,P,A,P ,Γ,∆)). % A is a procedure call 1 allows people to sign up for a mailing list. An example (4) ex(P,k(true),P). % True is always a success. ofthisclassisprovidedbythefollowingcodewherethe procedure below adds a person to a list: (5) ex(P,k(),P). % Empty threads mean a success. % Procedure signup (6) ex(P,k(Γ,x=E,∆),P ) ← 1 eval(P,E,E′) seqand % evaluate E to get E′ signup(person) = (ex(P ⊎{hx,E′i},k(Γ,∆),P ) 1 (N =N +1 ♯ list[N]=person) % critical section % If an assignment statement x = E is chosen by our interpreter, update x to E′ and return to the interpreter. Here,⊎denotesasetunionbuthx,Vi and the main program consists of two concurrent in P will be replaced by hx,E′i. threads as follows: (7) ex(P,k(Γ,;(),∆),P ) ← k(signup(tom),signup(bill)) 1 LETTER 3 In the above, we used a more traditional notation (G1♯,...,♯Gn) instead of ♯(G1,...,Gn). Although the above signup procedure is in fact a criticalsection,itworkscorrectlybecause nointerleav- ing – due to the presenceof ♯ –is allowedin the critical section. Note that our code is very concise compared to the traditional ones using semaphores. 4. Conclusion In this paper, we proposed a simple concurrent model for imperative languages. This model introduces a blocksequentialstatement♯(G1,...,Gn)whereeachGi is astatement. This statementexecutesG1,...,Gn se- quentially and atomically. It therefore enhances atom- icity and predictability. Althoughwefocusedonasimpleconcurrentmodel forimperativelanguageatasubprogramlevel,itseems possible to apply our ideas to existing concurrent and parallel computing models [1],[2]. 5. Acknowledgements This work was supported by Dong-A University Re- search Fund. References [1] J. Alglave and L. Maranget and M. Tautschnig, “Herding cats: Modelling, simulation, teating and data mining for weak memory”, ACM Transactions on Programming Lan- guages andSystems,vol.36,no.2,pp.1–74,2014. [2] G.BoudolandG.Petri,“Relaxedmemorymodels: anoper- ationalapproach”, InPOPL,pp.392–403, ACM,2009. [3] G. Kahn, “Natural Semantics”, In the 4th Annual Sympo- siumonTheoreticalAspectsofComputerScience,LNCSvol. 247,1987. [4] G.Japaridze,“Introduction tocomputabilitylogic”,Annals ofPureandAppliedLogic,vol.123,pp.1–99, 2003. [5] G.Japaridze,“Sequential operatorsincomputabilitylogic”, InformationandComputation,vol.206,No.12,pp.1443-1475, 2008. [6] K. Kwon, S. Hur and M. Park, “Improving Robustness via DisjunctiveStatementsinImperativeProgramming”,IEICE Transations on Information and Systems, vol.E96-D,No.9, pp.2036-2038, September, 2013. [7] J.HodasandD.Miller,“LogicProgramminginaFragment of Intuitionistic Linear Logic”, Information and Computa- tion,vol.110,No.2,pp.327-365,1994. [8] D.Miller,G.Nadathur,F.Pfenning,andA.Scedrov, “Uni- formproofsasafoundationforlogicprogramming”,Annals ofPureandAppliedLogic,vol.51,pp.125–157, 1991. [9] D. Miller, G. Nadathur, Programming with higher-order logic,CambridgeUniversityPress,2012.