說到要學電腦程式語言，Python相信是近年最炙手可熱的語言了，一來Syntax易學易用，二來library支援眾多，更是近期最熱門人工智能的主要語言，我最近因工作需要也要學Python。以前我讀大學時程式入門課教C，然後過幾了年進化為教Java，不過最近陸續轉為教Python了。公司新請回來的大學生個個都懂Python，吾等老海鮮也要與時並進才不會被淘汰。
原本公司內部個兩不同部門使用不同語言，chip testing和apps那邊以前用tcl，貪tcl不用compile方便操作，我們software testing那邊則以C++為主，因為需要OOP和static type來架構軟件測試系統。兩個部門有很多基礎的應用程式功能重壘，不過因為使用不同語言，同一個功能需要寫兩次。高層認為一code兩寫很沒有效率，下令我們統一使用同一語言，在雙方列出對語言的要求後，Python成為很自然的選擇。Python是interpreter language不用compile，同時又支援OOP和type checking，一次過滿足我們兩個部門的願望。
學習新程式語言，很多人喜歡讀網上課程，不過我比較傳統喜歡看書，我嫌網上課程看影片太嘥時間，看書容易明的部份可以速讀，難明的部份可以花多此時間重看幾遍。學習寫程式最重要是落手落腳寫code，跟課本的練習做同做網上課程的功課分別不大，反正程式寫得好就work有bug就唔work，沒有需要改功課對答案的問題。在芸芸眾多本Python書中，我挑選了這本《Head First Python》，看電腦書不是大大本很厚多字就好，最重要是把應用慨念解釋清楚，有時一張圖或一個例子可以抵得上三版紙枯燥的文字。這本書開宗明義不是教寫程式，而是寫給已懂其他語言的人學習Python語法。這本書最優勝之處的單元的編排，整本書就是寫一個有趣的小小網上應用程式，每章都教一些新東西為程式加上新功能，看書就好似一路做project咁不會悶。最怕有些程式書只是把語法由頭到尾列出來，再口水多過茶地加鹽加醋地長篇大論講解。
最初看Python很不習慣那個indent style，寫了咁多年程式都係用curly bracket, 唯有Python別樹一格強迫indent，不過寫幾個星期習慣了就不再覺得礙眼。同C++或Java比，Python同Ruby算是第四代的程式語言，去年學過Ruby所以Python很快上手，兩者的設計理念不同，不過最核心的本質其實一樣，明白了個背後用C寫的Ruby/Python個interpreter，睇埋個interpreter入面的internal data-structure，咁成個語言就一理通百理明。Ruby就乜都係object，Python雖然有人都係咁講，但我認為Python的真蒂其實乜都係callable，連class declaration都係一個function。明白了這一點後，Python所有新feature concept，如generator，declaration，context manager，future, asyncio等等就能清楚理解明白。
睇完本書跟住它做完個project仔，再上Python官網看一次官方tutorial，把standard library的所有API係咁意睇一次，大慨知道有乜function乜library可以用，遇到問題就問stack overflow大神求救，還有功能強大的PyCharm相助，其實Python很容易上手。越寫越覺得Python好使好用，大有相逢恨夜的感覺。現在學了用了Python兩個多月，自問至少追上公司新仔的水平，review佢地寫的code也不會失禮問白痴問題。
在PC上安裝Linux很簡單，上網下載個今期最新最流行的distribution，然後跟著畫面步驟照做就可以，基本上與安裝Windows同樣方便快捷。在embedded system上安裝Linux，就沒有這樣簡單了，embedded system規格千萬化，就算是使用同一塊晶片做CPU，不同的開發板也有不同設備。若果是熱門多人用的開發板（如Raspberry Pi, BeagleBoard等）還好，用家社群可以找到不同package的Linux系統，有些冷門的開發板就只有廠家提供的package，若果不適合或廠家不再更新，就要自已落手落腳去compile合用的Linux。
這本書2011年出版，當年Linux kernel版本還是2.6，現在已經去到4.14。在科技日新月異的電腦界，三四年已經面目全非，看這本六年前出版的「舊書」，內容會不會過時？其實作業系統的轉變非常緩慢，雖然每個版本的Linux也有新功能，但始終都是建立在UNIX架構基礎上，所有接近CPU硬件的低階知識都是累進的，畢竟CPU架構十多年來也沒有大變化呀。說到要從source code開始去compile Linux，網上料資一是太零碎一是太深，除非付費報名上堂去學，否則要靠這本書當指路明燈。不過這本書並非入門書，對讀者程度有頗高的要求，一是要對Linux作業環境有一定認識，二是要有寫程式和搞硬件的經驗，除非是工作需要或電腦科的學生，應該沒有人會自己compile Linux。
這本書的內容比之前看那本How Linux Works 更低階，首兩章講什麼是embedded system，其實會看這本書又怎會不知道，不過開場白總不能避免。第三章正式進入戲肉，講解kernel的source code的架構，粗略介紹如何config。這本不是講kernel的專題書，大部份compile Linux的人都不會改動個kernel，所以不用講太深入。之後兩章分別講kernel init同user space init，平時開機見kernel印一大堆message出來，終於知道那些message是什麼。這本書解釋root file system十分好，之前看其他地方了幾次解釋都看不明白，今次終於睇得明。另一章是教寫device driver亦是本書重點，用一個dummy drive做例子，可以跟著書照做自己試下寫。
之後的章節很有系統介紹整個embedded Linux需要用到的各種工具，從compiler到debugger到build system，讓讀者知道有什麼東西可供使用，然後可以自己google更進一步的資料，如何連名稱也不知道，想google也無從查起。原本我打算用Yocto去compile，不過經這本書提醒，再看看網上的比較資料，初學者還是用Buildroot較容易上手。
之前只是跑其他人寫落的script去compile kernel，感覺很不實在，完全不知道自己在做什麼，如果有什麼事唔work，只能叫人幫手整，自己完全幫不上忙。睇完這本書，我才覺得有足夠的知識，去應付工作上可能遇到問題。我有自知之明，我還未夠料親自落手落腳去fix問題，不過至少填寫bug report時，不用好白癡咁乜都只係識話唔work，至少識話俾人邊度唔work有乜野要fix。
接觸Linux大大話話都有廿幾年，從最初唔知買乜鬼雜誌送CD，自已裝來裝去到搞唔掂個graphics driver，到後來Linux一統江湖，日日返工都在Linux上寫code，到最近因工作需要自己compile Linux，才發覺我從來沒有認真學習過Linux。日常使用Linux跑程式，砌機灌OS裝Linux那些手板眼見功夫，遇到難題上網Google答案輕易過關，基礎打不好，現在書到用時方恨少，要有系統地重新認識Linux。
這本《How Linux Works》雖然美其名是入門書藉，不過除了第一章的Linux簡介，第二章日常使用的commands外，第三章打後難度三級跳，從Filesystems，到Kernel Bootup，systemd執行先後次序，每一個題目都超過一般用家要知道的知識，可以說是Linux admin的指南索引。這本書不太厚只有不到四百頁，所以每個題目都不會講得太深入，反而是系統化地把Linux的內容例出來，讀者大約知道有什麼題目，然後自己再找上網找資料。
這本書的內容，大慨有八成我以前看過，所以看過本書非常快，很多章節只是粗略翻看。剩下來的兩成新知識非常有用，補完我對Linux認知的缺漏，有些很簡單的基礎慨念，一般網上速食解答沒有講解，例如/usr其實同user無關，新process如何fork出來，shell script可以開subshell，X系統server同client的分功等等。很多東西我懂得用但不求甚解，現在學好了基本知識，開始看通Linux的設計邏輯，很多疑問便一理通百理明。
不過看完這本書，雖然對Linux的認識是完整了，對於compile Linux的幫助不大，頂多在我執package時至少知道放了什麼入去個build度，但解決不了kernel開不到機的燃眉之急，還要繼續找其他書看。
這篇不是書評，這本書亦不是一般自學程式設計的電腦書，是一本涉及非常專門的知識，只有設計晶片才會用得上的技術課本。非行內人完全看不明白，這篇只是我學習formal verification(形式化驗證)的心得和筆記，所以我亦不期望有什麼讀者。
什麼是Formal Verification？首先要講什麼是dynamic verification，設計晶片不同寫程式，寫程式有bug很簡單，除錯出patch沒有什麼大不了。晶片有bug就很大件事，因為要更正問題，就要重新tape-out多一次，去做一個全新的mask。可以想像製造晶片好印黑膠碟，先要整有一張母碟，然後才可以覆印，mask就是silicon的母碟。傳統上測式晶片設件主力用simulation（即dynamic verification)，要花很多人力物力寫個testbench出來，然後模疑晶片所有的input同output。這是一個非常嚴格的工序，因為一個bug也不可以走漏。晶片出了街之後，fix一個bug的成本是幾百萬美元。寫testbench同寫普通software沒有太大分別，只不過測試硬件比測試軟件嚴格很多。Formal Verification則是用另一個方法去測試硬件，不用寫code，寫formal specification，再用數學邏輯理論，去證明硬件的設件必定等於那個specification。完全不同的思考方法，完全不同的用途。Formal Verification可以測試出simulation找不出來的bug，始終simulation並不是exhaustive，不過formal有很多限制，設計不能太大不能太深，始終formal proof係一個NP-complete problem。
多年來formal一直只是學術研究，真正的商業應用，大約五六年前才開始。早期的formal tool非常難用，常常被戲說要博士才懂用，很多designer聽見便敬而遠之。直至JasperGold的推出，formal才開始普及化，這些年來JasperGold手執牛耳，一枝獨秀差不多等同於formal的代名詞。早兩年我也嘗試過學formal，不過當年JasperGold的license太貴，我們細公司買不起，只好用了一個很差很難用的IFV，結果學師未成不了了之。去年我公司被一個大公司收購了，economy of scale讓我們有多好多tools用，今個project終於有機會用到JasperGold，同IFV相比簡直是天堂和地獄，「工欲善其善，必先利其器」，其實formal一點也不難，我花了兩星期便滿師，可以學懂簡單的formal specify，去proof我個design不會有dead lock。如果要用simulation作同樣測試，因為太多corner cases，是一件非常痛苦的差事。現在用formal去做，幾行code寫完，是一件很好玩的玩意。
我一直都有follow開formal的paper和tutorial，雖然沒有實戰經驗但formal理論大至明白，用新tool不過是學syntax，很快上手。我公司的formal expert介紹我看這本《Formal Verification》課本，這本書是三位Intel工程師編寫的，由淺入深講解很有系統地如何應用formal verification，真正的hard-core技術含量不多（技術東西可以自已看document)，反而更像是過來人分享心得和經驗。這本書九成是老生常談，平時睇tutorial睇paper都學過聽過，不過餘下的一成非常有用，讓我茅塞頓開，很多看已paper不明白人家為什麼一定要這樣做的地方，經他一解釋完全明白，一理通，百理明。這本書可以說是我formal的啟蒙老師，任何一個初學formal者必定要看。市面上formal的textbook一隻手數得完，因為formal是太專門的技術，譎想想學就要交很貴學費請consultant去教，不過我認為這本書比consultant教得更好，因為作者有真正的實戰經歷，不似consultant般大多紙上談兵。
以下是我認為書中有用的formal「心法」：
cover和assert是同一塊鏡子的兩面。同一個property，cover就是not左個property的assert的counter example。assert就係not左個cover既unreachable proof
Formal engine係一個breath-first咁去行所有的state space。assume同assert就係cut細個state space，cut走左illegal state，如果行到去specification果個state，咪就proof度囉。
一開波不要立即寫full proof，先由cover開始玩。唔用assume，剩係寫你想睇乜output，睇下formal engine可不可以back trace你想要的input，然後再慢慢fine-tune那些assume
用cover整好晒assume，就可以上去bug hunting，專心搵assert的counter example，最後才整full proof。用之前兩個steps的assume
唔好load太多code，太多assert同cover，要divide and conquer。有些tricks可以用，如cutpoint，abstraction，free variable等等
在很多大學中，電腦系不是附屬於工程學院，便是附屬於科學院。我以前讀的大學很奇怪，電腦系是附屬於數學院，當年我不明白原因，電腦可以用來計數，但電腦和數學有什麼關係呢？我是讀電腦工程系出身的硬件人，當年與電腦科學的同學談起，聽他們說電腦理論很難明高呼救命，天真的我以為讀電腦科學不就是學寫程式嘛，有多難？直至很多年以後，某次去印度工幹買了這本《電腦理論入門》，丟在書架上又過了幾年，然後某天心血來潮打開來看看，前後繼繼續續花了兩年多才看完，終於我明白原來電腦理論不等於電腦，而是數學上如何械械式解答問題的定律。
這本Daniel I.A. Cohen的《Introduction to Computer Theory》，是電腦理論的經典課本。某種意義上，這本書非常沉悶，全本書就好似中學讀數學不停學proof。從最簡單的regular expression開始proof，一路到finite automata，到context-free grammer和pushdown automata，最後就是頂頂大名的萬能電腦原形Turing Machine。證明什麼類形的電腦可以接受什麼類形的language，某notation又可以如何與某graph等同互換。最精彩的章節是詳細解釋Turing Machine，以前上堂聽過這個term，記得教授說過TM是萬能電腦，看完這本書後，終於明白為什麼TM可以計到任何可以計得到的數，即可以解答任何能找出答案的問題。再一次佩服Alan Turing的天材，TM的構造極其簡單，可是沒有任何機械能超越TM的解題能力。
最初開始讀這本書時，我不明白language同電腦有什麼關係，不就是一串串不同的string，起個state machine去判斷一個input是否屬於language之內，程序上是有點麻煩不過也不是很複雜，要用咪call library囉。去到context-free grammer開始看到有點關係，至少寫compiler的第一步就是要parse個syntax tree。一直以無比的耐心閱讀著，逐步逐步follow書中的proof，然後有一天開竅了，忽然間看到language和solve problem之間的關係，任何能夠解答的問題都是一個數學題，電腦就只是從機械化地處理input，然後給一個output的系統，output可以是答案，但更多時間只是一個yes/no answer，又或者更基本的halting problem。找出一個問題的答案，只是最表面那層，找出一問題有沒有可能有答案，如果有答案的話，有限時間內能否找到，那些bounding的meta問題，才是電腦理論的核心。至於如何寫個行得快些慳位些的algorithm去解題，已經是應用層面上技術性的次要問題。
若果不打算理會那些proof，這張圖表大慨是全書內容的總結。老實說那些proof讀完大部份都忘記了，能夠記得大慨就只有這圖表的內容。不過讀proof的最大得著，是讀proof會潛移默化你腦袋的思路，看完知道的東西和未看差不多，但再遇同類問題時會有一份直覺。
初版pdf下載 ，我看的是第二版實體書。
Posts navigation
蘋果日報作者 – 陳馬：書評，影評，動漫，旅行，哲學筆記
