ATLANTIS STUDIESINCOMPUTING VOLUME2 SERIESEDITORS: JANA.BERGSTRA, MICHAELW.MISLOVE Atlantis Studies in Computing SeriesEditors: JanA.Bergstra MichaelW.Mislove InformaticsInstitute DepartmentofMathematics UniversityofAmsterdam TulaneUniversity Amsterdam,TheNetherlands NewOrleans,USA (ISSN:2212-8565) Aimsandscopeoftheseries Theseriesaimsatpublishingbooksintheareasofcomputerscience,computerandnetwork technology,ITmanagement,informationtechnologyandinformaticsfromthetechnologi- cal,managerial,theoretical/fundamental,socialorhistoricalperspective. Wewelcomebooksinthefollowingcategories: Technicalmonographs:thesewillbereviewedastotimeliness,usefulness,relevance,com- pletenessandclarityofpresentation. Textbooks. Booksofamorespeculativenature: thesewillbereviewedastorelevanceandclarityof presentation. Formoreinformationonthisseriesandourotherbookseries,pleasevisitourwebsiteat: www.atlantis-press.com/publications/books AMSTERDAM–PARIS –BEIJING (cid:2)c ATLANTISPRESS Instruction Sequences for Computer Science Jan A. Bergstra and Cornelis A. Middelburg InstituteofInformatics,FacultyofScience, UniversityofAmsterdam Amsterdam,theNetherlands AMSTERDAM–PARIS –BEIJING AtlantisPress 8,squaredesBouleaux 75019Paris,France ForinformationonallAtlantisPresspublications,visitourwebsiteat:www.atlantis-press.com Copyright Thisbook,oranypartsthereof,maynotbereproducedforcommercialpurposesinanyformorby anymeans,electronicormechanical,includingphotocopying,recordingoranyinformationstorage andretrievalsystemknownortobeinvented,withoutpriorpermissionfromthePublisher. AtlantisStudiesinComputing Volume1:CodeGenerationwithTemplates-B.J.Arnoldus,M.G.J.VandenBrand,A.Serebrenik ISBNs Print: 978-94-91216-64-0 E-Book: 978-94-91216-65-7 ISSN: 2212-8565 (cid:2)c 2012ATLANTISPRESS Preface Theconceptofaninstructionsequenceisakeyconceptinpractice,butstrangelyenough it has as yet not come prominentlyinto the picture in theoreticalcircles. In much work oncomputerarchitecture,instructionsequencesareunderdiscussion. Inspiteofthis,the notionofaninstructionsequencehasneverbeensubjectedtosystematicandpreciseanal- ysis. Moreover, in work on computer architecture, the viewpoint is usually taken that a programisinessenceaninstructionsequence. Bycontrast,inthetheoryofcomputation, differentviewpointsonwhatisaprogramareusuallytaken. Thisstateofaffairsbrought usto definea generalnotionofaninstructionsequence,to subjectit toa systematic and preciseanalysis, andtoprovideevidenceforthehypothesisthatthenotionofaninstruc- tionsequenceisrelevanttodiversesubjectsfromthetheoryofcomputationandthearea ofcomputerarchitecture.Manyresultsoftheworkinquestionarebroughttogetherinthis bookwiththeaimtobringinstructionsequencesasathemeincomputersciencebetterinto thepicture. Toputitotherwise,thisbookconcernsinstructionsequences,thebehavioursproduced by instruction sequences under execution, the interaction between these behaviours and componentsof the execution environmentconcerning the processing of instructions, the expressiveness of instruction sequences, and various issues relating to well-known sub- jects from computer science where we found that the notion of an instruction sequence is relevant. Most of the issues in question are of a computation-theoretic or computer- architecturalkind. Theyrelatetosubjectssuchasthehaltingproblem,non-uniformcom- putationalcomplexity,instruction sequence performanceand instruction set architecture. Someoftheissuesconsideredaresomehowrelatedtoprocessalgebra,namelyremotein- struction processing and instruction sequence producible processes. Some variations on instructionsequencesoftheusualkind,suchasinstructionsequenceswithoutadirectional biasandprobabilisticinstructionsequences,arealsoconsidered. v vi InstructionSequencesforComputerScience This book is primarily intended for researchers in computer science interested in in- struction sequences as a theme in computer science. It is also meant to be suitable as supplementaryreadingin coursesforgraduatestudentsand advancedundergraduatestu- dentsincomputerscience.Chapters5and6mayasmuchappealtothosewhoareprimarily interestedinthesubjectsfromthetheoryofcomputationandtheareaofcomputerarchitec- ture,respectively,thatcomeupinthesechapters. Chapter7mayasmuchappealtothose whoareprimarilyinterestedinprocessalgebra. Throughoutthe book, some familiarity with equational logic, universal algebra, and elementaryset theory is assumed. In Sect. 5.2, some familiarity with non-uniformcom- putational complexity is assumed. In Sect. 5.1, Sect. 6.2 and Chap. 7, some familiarity with computability,instruction set architecturesand processalgebra, respectively, would behelpful. Chapter2isaprerequisiteforChap.3,andbothchaptersareprerequisitesfor allsubsequentchapters. Chapter 2 introducesan algebraic theorySPISA of single-pass instructionsequences and an algebraic theory BTA of mathematical objects that represent in a direct way the behavioursproducedbyinstructionsequencesunderexecution.Theobjectsconcernedare called threads. Itis madeprecise in thesetting of the latter theorywhich behavioursare producedbytheinstructionsequencesconsideredintheformertheory.Theinstructionse- quencesinquestionincludebothfiniteandinfiniteones,butthetheoryprovidesanotation by means of which all of them can be represented finitely. This chapter also introduces alternative notations ISNR and ISNA by means of which all these instruction sequences canberepresentedfinitelyaswell,butwhichareclosertoexistingassemblylanguages. Chapter 3 introducesso-called services, which representthe behavioursexhibitedby thecomponentsofanexecutionenvironmentthatarecapableofprocessingparticularin- structions and doing so independently, and extends BTA with an operator meant for the compositionoffamiliesofnamedservicesandoperatorsthathaveadirectbearingonthe processing of instructions by services from such service families. In addition, the con- cept of a functionalunit, which is an abstractmodelof a machine, is introduced. In the frequently occurring case that the behaviours represented by services can be viewed as thebehavioursofamachinein itsdifferentstates, theservicesconcernedarecompletely determinedbyafunctionalunit. SomeextensionsofISNRandISNAwithadditionalin- structionsareexplainedwiththehelpofsomesimplefunctionalunits. Chapter4givesanswerstobasicexpressivenessissuesregardingSPISA. Inthiscase, expressiveness is basically about which behaviours can be produced by instruction se- Preface vii quencesunderexecution,whichinstructionscanberemovedwithoutreducingtheclassof behavioursthatcanbeproducedbyinstructionsequencesunderexecution,howtoenlarge theclassofbehavioursthatcanbeproducedbyinstructionsequencesunderexecution,et cetera. Thischapter is also concernedwith some issues thatarise fromthe investigation ofexpressivenessissuesregardingSPISA. Forexample,itisshownthatafinite-stateexe- cutionmechanismforasetofinstructionsequencesthatbyitselfcanproduceeachfinite- statebehaviourfromaninstructionsequencebelongingtothesetofinstructionsequences inquestionisunfeasible. Chapter 5 concernstwo subjectsfrom the theoryof computation, namely the halting problemandnon-uniformcomputationalcomplexity.PositioningTuring’sresultregarding theundecidabilityofthehaltingproblemasaresultaboutprogramsratherthanmachines, andtakingsingle-passinstructionsequencesasconsideredinSPISAasprograms,theau- tosolvabilityrequirementthataprogramofacertainkindmustsolvethehaltingproblem for all programs of that kind is analysed. Thinking in terms of single-pass instruction sequencesas consideredin SPISA, counterpartsof the classical non-uniformcomplexity classesP/polyandNP/polyaredefined,anotionofcompletenessforthecounterpartof NP/polyisintroduced,severalcomplexityhypothesesareformulated,anditisshownthat aproblemcloselyrelatedto3SATisNP-completeaswellascompleteforthecounterpart ofNP/poly. Chapter 6 concerns two subjects from the area of computer architecture, namely in- struction sequence performanceand instruction set architectures. We study the effect of eliminatingindirectjumpinstructionsfrominstructionsequenceswithdirectandindirect jumpinstructionsontheinteractiveperformanceofinstructionsequences.Astrictversion oftheconceptofaload/storeinstructionsetarchitectureisproposedfortheoreticalwork relevant to the design of instruction set architectures, and it is studied how the transfor- mationsonthestatesofthemainmemoryofastrictload/storeinstructionsetarchitecture that can be achieved by executing instruction sequences on it depend on the parameters involved. Chapter7 concernstwo subjectsrelated to processalgebra, namelyprotocolsto deal with remote instructionprocessing and instructionsequence producibleprocesses. If in- struction processing takes place remotely, this means that a stream of instructions to be processedarisesatoneplaceandtheprocessingofthatstream ofinstructionsishandled atanotherplace. Processalgebraisusedtodescribetwoprotocolstodealwiththisphe- nomenon. Becauseprocessalgebraisconsideredrelevanttocomputerscience,theremust viii InstructionSequencesforComputerScience beprogrammedsystemswhosebehavioursaretakenforprocessesasconsideredinprocess algebra. Itisshownthatallfinite-stateprocessescanbeproducedbysingle-passinstruc- tionsequencesasconsideredinSPISA,providedthattheclusterfairabstractionruleknown fromthealgebraictheoryofprocessescalledACPisvalid. Chapter8introducesthreevariationsofinstructionsequencesasconsideredinSPISA, namely polyadic instruction sequences, instruction sequences without a directional bias, andprobabilisticinstructionsequences. Apolyadicinstructionsequenceisapossiblypa- rameterizedinstructionsequencefragmentthatcanproduceajointbehaviourtogetherwith other such fragmentsbecause the fragmentbeing executed can switch over executionto another. Instructionsequenceswithoutadirectionalbiasrequirethatforeachinstruction whoseeffectinvolvesthatexecutionproceedsintheforwarddirection,thereisacounter- partwhoseeffectinvolvesthatexecutionproceedsinthebackwarddirection.Probabilistic instructionsequencesareinstructionsequencesthatcontaininstructionsthatarethemselves probabilisticbynature. Therearealso fourappendices. InAppendixA, fivechallengesforthepointofview fromwhichtheapproachtosemanticsfollowedinChaps.2and3originatesaresketched. InAppendixB,someresultsaboutfunctionalunitsfornaturalnumbersaregiven,whichare exceptonecomputabilityresultsthatarenotdirectlyrelatedtoexistingresultsthatweknow of. InAppendixC,theusefulnessofthedynamicallyinstantiatedinstructionsintroduced inChap.3isillustratedbymeansofanexample.InAppendixD,amodelofahypothetical executionenvironmentfor instruction sequences, designedfor the purpose of explaining howinstructionsequencesasconsideredinSPISAmaybeexecuted,isdiscussed. Aglossaryofthenotationsintroducedinthisbookandthegeneralmathematicalno- tationsusedin thisbookcan befoundfrompage221onward. Atthispoint, onefurther remarkaboutnotationmaybeuseful:bold-faceditalicletters,withorwithoutdecorations, willbeusedassyntacticalvariablesinthisbook. Acknowledgements Thisbookbringstogetherandstreamlinesworkdonebyagroupofpeoplewhichincludes, in addition to the authors, Inge Bethke, Marijke Loots, Alban Ponse and Mark van der Zwaag. Theworkinquestionwaspartlycarriedoutintheframeworkofprojectsfunded bytheNetherlandsOrganisationforScientificResearch(NWO). Amsterdam,April2012 J.A.BergstraandC.A.Middelburg Contents Preface v ListofTables xv 1. Introduction 1 2. InstructionSequences 5 2.1 SinglePassInstructionSequenceAlgebra . . . . . . . . . . . . . . . . . 5 2.1.1 Primitiveinstructions . . . . . . . . . . . . . . . . . . . . . . . 6 2.1.2 Constants,operatorsandequationalaxioms . . . . . . . . . . . 7 2.1.3 Theinitialmodel. . . . . . . . . . . . . . . . . . . . . . . . . . 9 2.1.4 Structuralcongruence . . . . . . . . . . . . . . . . . . . . . . . 10 2.2 BasicThreadAlgebra . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12 2.2.1 Constants,operatorsandequationalaxioms . . . . . . . . . . . 12 2.2.2 Recursion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14 2.2.3 Regularthreads . . . . . . . . . . . . . . . . . . . . . . . . . . 16 2.2.4 Theprojectivelimitmodel . . . . . . . . . . . . . . . . . . . . 18 2.2.5 Threadextractionforinstructionsequences . . . . . . . . . . . . 21 2.2.6 Behaviouralequivalenceofinstructionsequences . . . . . . . . 23 2.3 InstructionSequenceNotations . . . . . . . . . . . . . . . . . . . . . . . 25 2.3.1 TheinstructionsequencenotationISNR . . . . . . . . . . . . . 26 2.3.2 TheinstructionsequencenotationISNA . . . . . . . . . . . . . 28 2.3.3 Inter-translatabilityofISNRandISNA . . . . . . . . . . . . . . 30 2.3.4 Additionalinstructionsequencenotations. . . . . . . . . . . . . 30 ix