赵翔鹏的Blog Xiangpeng's Thinkpad

Path to Salvation

子贡曰：“我不欲人之加诸我也，吾亦欲无加诸人。”子曰：“赐也，非尔所及也。”

破除幻想，何以解困？

经云：

“自为洲渚。自为归处。
法为洲渚。法为归处。
无别洲渚。无别归处。”

法之为筏，故“自”为首。明心见月，即得自在。

五台游记

有些地方像铅笔画，去过之后，留下的是单色直截的回忆。大多数城市都是这样，灰蒙蒙的，大同小异；有些地方像水彩画，有着鲜明的色彩，印象很浓烈地涌动在心中，却几乎不能用言语描述。五台山是这样的地方。

五台山以清凉闻名。又因为是文殊菩萨的道场，更有智慧加持。此地有青山和白云为伴，天晴时气势雄浑，以大白塔为最，游者自生敬畏之心。雨来则柔和清丽，水气染湿了屋檐，碧山寺里嫩黄的菊花滴着微凉的水珠，心至妙境，难以述说。找个蒲团静坐半晌，看青山之外的一重重云山，真如诗中所说的，“相看两不厌”。

五山环抱着大大小小的寺庙，青砖白塔，黄瓦碧天，苍柏遍地。每座寺庙都有自己的故事。有些香火鼎盛，人流熙攘，有些清冷静寂，罕有客至。在塔院寺的白塔下，黛螺顶的石阶上，显通寺门外匆匆的游客脚步边，有修行者长跪于地，三步一叩，亦有端着小筐讨钱的假人。此众生相，文殊当知。

五台各供有一座文殊。西台狮子吼文殊，北台无垢文殊，中台孺童文殊，南台智慧文殊，东台聪明文殊。因为第二日有雨，原计划的登山只好取消，不过黛螺顶上的五方文殊像也可满足朝台者的心愿。黛螺顶上有一只大狗，长相凶猛，有铁链拴着，却出人意料的温顺。旁边有位慈眉善目的居士阿姨念着佛号抚摸其头顶，给我们讲了个轮回的事迹，或者故事。故事的细节并不重要。那沉静透彻的眼神，是我所难忘的。

捐了香火给北台，许下个愿。清凉寂静，烦恼不现，众苦永寂。如此境界或不可求，却可在五台山望到了。不知何时会再来呢？

---------------美好和现实的分界线------------------------

五台山的很多地方是喧闹的，也有很多人是找你要钱来的；包括一些僧人。
还好这不妨碍建筑物本身的美，何况，在路上确实遇见一些真正的信徒。从藏区赶来的人几乎都很动人，无论是穿百衲衣磕长头皮肤晒得黝黑的僧人，还是似乎是头一次吃到冰淇淋的藏族小女孩，还有她不会说汉语的妈妈。

“流于事项”，在走过、看过一个接一个似乎大同小异的泥塑金身之后，确实有点这个感觉。庄严但是缺乏深度，好像是执客僧的脸。所以我觉得最喜欢的是塔院寺的大白塔和碧山寺的雨中菊花。

平遥的物质条件很好，玩得也很开心，但心灵的感受还是不及五台山。这两个地方的区别，大概就是市民生活跟大学教授的区别吧。

周末须读书

我见黄河水，凡经几度清。
水流如激箭，人世若浮萍。
痴属根本业，爱为烦恼坑。
轮回几许劫，不解了无明。
寒山出此语，举世狂痴半。
有事对面说，所以足人怨。
心真语亦直，直语无背面。
君看渡奈何，谁是喽罗汉。
寄语诸仁者，仁以何为怀。
归源知自性，自性即如来。

今天上午读书。后来偶然搜到黄山谷书作及生平，一观之下，真是心境相若。以前虽也看过山谷书法，却不懂得欣赏；如今豁然开朗了。

此诗非黄庭坚所作，作者是寒山法师。黄庭坚所书，比原始诗意略增生气，却正如歌者咏唱经卷诗词，更能通俗。既是入世之作，又指出世之途；于是反倒更能感动人了。

点滴

关于摄影

我们为什么喜欢摄影？为什么不管别人的长焦镜头片子有多好，也抵不过自己的卡片机？

“无他，只是为了亲身体会透过镜头，如透过心灵之眼，将所见景色聚焦和记录。用来在以后的时光里反复揣摩和回忆一座城市。那些色彩的碎片，便是天长地久了。”

这个总结真完美。

关于专业书籍

这件事几乎是常识，但我还是忍不住感叹一下。

《面向计算机科学的数理逻辑：系统建模和推理》是一本好书。跟所有的国外书籍一样，作者会近乎唠叨地跟你解释一切问题背后的动机(motivation)，举出种种有趣的小例子，就为了让你明白，为什么要引入这个概念？为什么这个定理在计算机科学中很重要？

这些解释都是国产书里难以看到的，国产书更常见的是堆积如山的符号和证明。虽然在课上，好的老师会告诉你这些背后的故事。

为什么会这样呢？

关于音乐

外文歌曲一定要有适当的翻译、解释才可领略。比如NightWish的《Nemo》，其实跟海底总动员一点关系都没有。Rammstein的歌几乎都很不错。放个歌词网站在此。不知道有多少人也喜欢听这个？

爱好

爱好不能充饥，也不能换银子；其功能在于自娱，在于抒怀。

我自知画得不好，写字亦不专业。然而无论好坏，热情是一样的。爱是一样的。虽说做不成泉水一般的人，偶尔有热情时，理工男也可临时变身小喷泉吧。

写字画画本是无心的，贴出来，有点自曝隐私的意思。不过想想这爱好如果还能娱人，也算是多了它一个功用了。

某日加班时在会议室画的。有四色油笔，挺好用。

32位和64位的麻烦

如果没有8G内存，还是不要装64位的Windows。今天又被折腾了一下。

装了个淘宝旺旺，店主发了个链接，我打开之后拍下宝贝去付款，IE反复提示安装控件，但怎么都装不上。而且还看到提示某SmartCard驱动无法安装。重启了一下还是不行，连网上银行都出毛病了，以前明明是好的啊。

这时忽然发现任务栏上有两个IE图标。。。

原来淘宝旺旺里面的链接会默认打开64位的IE。难怪安全控件会不兼容。还好是用Windows7，有图标分组的功能。如果不是看到两个IE图标，我估计还得折腾半天。看了一下，旺旺倒是32位的。不知道做旺旺的人是咋整成这样的。

最后说一个常见的误解。如果有4G内存，虽然32位的系统会导致部分内存无法访问，也许只能用到3.0-3.5G的内存，但其实你换成64位的系统之后未必就提高了内存的使用效率。以前一个指针占32bit，换成64位后每个指针都大了一倍，所以每个程序都会占更多的内存，最终又还回去了。再考虑到种种潜在的兼容性问题，还是用32位安心啊。

人能完全认识自己吗。。。

最近又做了一次MBIT性格测试。上次是在单位的training中做的，带了太多工作的风格，结果是ENTP。这次的结果是INFP，应该更接近本我。

性格测试有意义吗？至少对我这种INFP的人而言是有的。可以把自己拎清楚点，用专业的话说，这叫self-awareness。

抄一段INFP Relationships，再教育一下自己——个人觉得，这段评价是字字见血啊……

INFPs present a calm, pleasant face to the world. They appear to be tranquil and peaceful to others, with simple desires. In fact, the INFP internally feels his or her life intensely. In the relationship arena, this causes them to have a very deep capacity for love and caring which is not frequently found with such intensity in the other types. The INFP does not devote their intense feelings towards just anyone, and are relatively reserved about expressing their inner-most feelings. They reserve their deepest love and caring for a select few who are closest to them. INFPs are generally laid-back, supportive and nurturing in their close relationships. With Introverted Feeling dominating their personality, they're very sensitive and in-tune with people's feelings, and feel genuine concern and caring for others. Slow to trust others and cautious in the beginning of a relationship, an INFP will be fiercely loyal once they are committed. With their strong inner core of values, they are intense individuals who value depth and authenticity in their relationships, and hold those who understand and accept the INFP's perspectives in especially high regard. INFPs are usually adaptable and congenial, unless one of their ruling principles has been violated, in which case they stop adapting and become staunch defenders of their values. They will be uncharacteristically harsh and rigid in such a situation.

INFP Strengths

Most INFPs will exhibit the following strengths with regards to relationship issues:

• Warmly concerned and caring towards others
• Sensitive and perceptive about what others are feeling
• Loyal and committed - they want lifelong relationships
• Deep capacity for love and caring
• Driven to meet other's needs
• Strive for "win-win" situations
• Nurturing, supportive and encouraging
• Likely to recognize and appreciate other's need for space
• Able to express themselves well
• Flexible and diverse

INFP Weaknesses

Most INFPs will exhibit the following weaknesses with regards to relationship issues:

• May tend to be shy and reserved
• Don't like to have their "space" invaded
• Extreme dislike of conflict
• Extreme dislike of criticism
• Strong need to receive praise and positive affirmation
• May react very emotionally to stressful situations
• Have difficulty leaving a bad relationship
• Have difficulty scolding or punishing others
• Tend to be reserved about expressing their feelings
• Perfectionistic tendancies may cause them to not give themselves enough credit
• Tendency to blame themselves for problems, and hold everything on their own shoulders

老师说，性格并不是永恒不变的。我的感觉是，I和E、F和T会在成长中变化，不过N/S和P/J貌似是天生的。

p.s. 昨晚忽然想画只猫，不过画完之后觉得更像自己……自己看画，觉得画也在看自己。

你站在窗口看风景，

看风景的人在桥上看你；

明月装饰了你的窗户，

你装饰了别人的梦

香茶余韵

品茗之美，越发觉得与红酒类似，然而又胜之。燃起一支檀香，藤台上，润润的紫砂壶里随着水流声荡漾开极品茶叶的韵味。灯光不可太亮白，非要暗淡到看不清角落里挂落的绿藤是真是假。说话都不可太紧迫，怕打破了这景致。

精致之极。

有故事的香茗，有故事的茶具，有故事的人，尽情体悟人生香醇微涩的美好，然后沉醉。金骏眉回甘香艳如唐寅的诗书，大红袍味正可比柳公权的法度，碧螺春清气如米芾侧锋的敏锐，普洱温醇养人则像了颜鲁公厚润。沉醉，沉醉，这一方书斋唤起桃源的梦。

不可过度。如再多品几种，那回忆就难以深刻了。回忆也不可太多。转为文字，已经心满意足。

Bill Gates与Joel Spolsky对形式化方法的评价

Billg对formal methods的评价是我第一次看到。跟Joel Spolsky的评价对比一下，很有趣。

1、Microsoft 的 SDV 经验：通过静态验证提高 Windows Vista 驱动程序的质量

Static Driver Verifier (SDV) 是一种基于规则的编译时静态分析工具，用于验证用 C 代码编写的 Windows 驱动程序。SDV 根据使用 Windows 设备驱动程序接口的精确规则集对驱动程序进行验证，然后报告这些规则的任何违规行为。

Microsoft Research (MSR) Software Productivity Tools 小组投入了多年的工作来创建一种引擎，以便自动检查基于 C 的程序是否正确使用与外部库相连的接口。此项目在 MSR 中称为 SLAM，最终的成果是一个已经集成到 SDV 的强大分析引擎。

以下引用了 Microsoft Research 小组的话，来自 MSR 网站上的“提供用于技术转移的模板”：

• 选择问题。“我们选择了一个重要但并非不能克服的问题领域进行研究（设备驱动程序）。……我们有机会了解 Windows 源代码和设备驱动程序源代码。此外，我们还能够广泛接触设备驱动程序和 Windows 领域的一流专家”。

• 站在巨人的肩膀上。“SLAM 拥有几十年使用正式方法和编程语言进行研究的经验。我们非常庆幸，在 Microsoft Research、Windows Division 以及 Microsoft 之外有许多人为 SLAM 和 SDV 出策出力”。

• 研究环境。“Microsoft 的产业研究环境以及普遍的动手/实干氛围使我们能够放手尝试使用危险的解决方案来解决重大问题，还可以提供我们迫切需要的支持。”

• 软件工程。“我们采用‘开放式’的体系结构风格来开发 SLAM，对每个核心组件使用非常简单的概念接口。这使我们能够迅速使用各种工具进行试验，设定一套我们认为最能解决问题的算法。这种体系结构使我们很容易对各种组件进行重新配置以对新问题做出反应。”

• 在工作中使用正确的工具。“我们使用法国研究机构 INRIA 的 Objective Caml 函数编程语言开发 SLAM。该语言的表达力及其实现的稳定性极大地提高了生产效率。”

SDV 目前在 Microsoft 内部使用，在 WDK 的测试版本中也提供了这种工具。它的宗旨在于使 Microsoft 及其合作伙伴能够提供高质量的设备驱动程序。

比尔盖茨在 OOPSLA 2002 上的发言：

为了进行丰富的静态分析，我们已经开发了许多东西。实际上，我们花了 3000 多万美元请其他公司开发此类工具，现在我想说的是，希望您们将精力集中在将这些工具应用于大规模软件系统上，在 Windows 或 Office 的源代码中都包含此种系统，看看到我们到底能取得什么样的进展。

让我们回顾一下，就证实程序是否以特定方式运行的能力来说，有哪些尖端技术？几十年来，这种问题一直存在。当我从哈佛退学时，这曾是一个让我感兴趣并努力解决的问题，实际上当时我还在想，如果我去开一家公司，情况可能会十分糟糕，我会错过在软件程序检验方面的一些重大突破，因为我需要忙于处理员工的工资单。事实证明，看来我还并未错过太多（笑着说道），我想说的是，在某种程度上，这已经是一个非常紧迫的问题。虽然不可能实现一种完全通用的解决方案，但是对于许多非常有趣的特性，这种检验的思想已经成为可以帮助我们的长效方法，仅在去年这一点已经得到充分的体现。

我们称执行这种检验的系统为模型检查系统。您需要定义约束，包括很简单的事情：已经获取锁的人不得再次获取；没有获取锁的人不得释放锁；以及您想要确定其运行良好的代码多线程方面的内容。在本例中，您使用 C 代码本身去描述这些，然后分析程序会仔细检查并缩减程序，去掉不影响其路径分析的任何内容，进行路径分析来确定整个程序中是否有路径违反约束。

我们首次应用此解决方案的领域是设备驱动程序。

第 17 届年度 ACM 讨论会 - 面向对象的编程、系统、语言和应用程序

2、《软件随想录》：Joel Spolsky对计算机学生的七大建议

我依然清楚记得我发誓绝不读研究生的那一刻。那是在一门叫做“动态逻辑”的课程上，教师是活力十足的耶鲁大学教授Lenore Zuck，她是计算机系那些聪明的老师中最聪明的人之一。

如今， 由于记忆力糟糕， 我已经差不多把这门课的内容忘光了，但是不管怎么说，在这里我还是想要对付着说一下。大致上，形式逻辑的意思是说，如果条件成立，你就能证明结论也成立。比如，根据形式逻辑，已知“只要成绩好，就能被雇用”，然后假定“Johnny的成绩好”，你就可以得到一个崭新的结论“Johnny会被雇用”。这完全是经典方法。但是，一个解构主义者（deconstructionist）只需要10秒钟就能破坏形式逻辑中所有有用的东西。这样一来，留给你的只是一些趣味性，而不是实用性。

现在再来说动态逻辑。它与形式逻辑其实是一回事，但是必须再多考虑时间因素。比如，“你打开灯之后，就能看见自己的鞋子”，已知“灯以前是亮的”，那么这就意味着“你看见了自己的鞋子”。

对于像Zuck教授那样聪明的理论家，动态逻辑充满了吸引力，因为它看上去很有希望让你在形式上证明一些计算机程序的相关理论问题。这样做说不定很有用。比如，你可以用它在形式上证明，火星漫游车的闪存卡不会发生溢出（overflow）问题，不会因而整天一遍又一遍地重启，耽误了它在那颗赤红色的星球上漫游寻找火星人马文（Marvin the Martian）。

在第一堂课上，Zuck博士写满了整整两面黑板，甚至黑板旁边的墙上都写上了很多证明步骤。需要证明的问题是，有一个控制灯泡的开关，现在灯泡没有亮，这时你打开了开关，请证明灯泡将会点亮。

整个证明过程复杂得不可思议，处处都是陷阱，必须十分小心。保证这个证明不出错太困难了，还不如直接相信打开开关灯就会亮。真的，虽然证明过程写满了许多块黑板，但是还是有许多中间步骤被省略了，因为如果要从形式逻辑上完整证明所有步骤，那就琐碎得无法形容了。许多步骤是用各种经典的逻辑证明方法推导得到的，包括归纳法、反证法等，甚至有些部分还是由旁听的研究生证明的。

留给我们的课后作业是证明逆命题：如果灯原来是关着的，现在却亮了，那么请证明开关的状态一定同原来相反。

我动手开始证明，我真的去证明了。

我在图书馆里待了很长时间。

我对照着Zuck博士的原始证明想依样画葫芦。研究了几个小时之后，我在其中发现了一个错误。可能我抄写的时候抄错了，但是这使得我想通了一件事。如果花费3个小时，写满了一块又一块的黑板，每一秒钟都可能出错，最后能够证明的却只是一个很琐碎的结论，那么这种方式有多大的实用性呢？在活生生、充满趣味的现实世界中，你永远都不会有机会使用它。

但是，动态逻辑的理论家们对这一点不感兴趣。他们看上它不是因为它有用，而是因为它可以为他们带来终身教职。

我放弃了这门课，并且发誓绝不会去读计算机科学的研究生。

这个故事告诉我们，计算机科学与软件开发不是一回事。如果你真的非常幸运，你的学校可能会开设很像样的软件开发课程。但是另一种可能是，你的学校根本不教你在现实中如何编程，因为精英学校都觉得，教授工作技能最好留给职业技术学校、犯人重返社会的培训项目去做。你到处都能学怎么写代码。别忘了，我们是耶鲁大学，我们的使命是培养未来的世界领袖。你交了16万美元的学费，却在学循环语句的写法，这怎么可以？你以为这是什么地方，难道是机场沿途的酒店里临时拼凑起来不靠谱的Java语言培训班？哼哼。

麻烦在于我们没有一种真正教授软件开发的专门学校。你如果想成为一个程序员，你可能只能选择计算机科学专业。这是一个不错的专业，但是它同软件开发不是一回事。在那些400等级的课程代号中，去寻找名称中带有“Practicum”这个词的课程吧（编者注：指供人实习的课程）。不要被这个拉丁语单词吓倒，这些都是有用的课程，之所以起这种名字，只是为了让那些文绉绉、装腔作势、满嘴胡说八道的公司经理们觉得高深莫测。

做完了Web service，形式化方法再能做点啥？

作为一个毕业许久的人……谈起纯学术有点偏离当前本职工作的意思。不过想想这些事情还是比较有意思的。

Web service折腾了许多年，似乎已经来到了拐点。由ICWS一再延长submission date可见一斑。从理论上看，好做的都做了，没做的corner越来越少了。

再做什么呢？

云计算是一种新的商业模式，可能带来巨大利润，所以业界极为关注。但对于计算机理论研究而言恐怕没那么多新元素。虚拟化的服务器，是很好的实现技术。可它既然已经是“虚拟”的，那么形式化方法常见的abstraction思想就没有用武之地了。

当然也要想到，SOA跟RPC相比，似乎也没那么多新元素，却做出了那么多的paper……这里应该总可以找到些可以做的地方。再仔细想想。列为TODO。

无线传感器网络是个有趣的领域。与形式化方法结合，可以做一些验证的工作，比如传输协议。不过，这跟p2p可能会很像。如果早几年了解到这个领域就好了。

graphics、search、social network这些领域跟形式化方法天生就没有关系……凡是需要heruistics和statistics的地方，没法用简单的逻辑描述，就基本没有形式化方法的事儿。然而越是貌似不可能的地方，越可能隐藏着尚未发掘的矿产……虽然不好说是金矿还是铜矿。

最后，performance tuning和操作系统。一直觉得这里很有可做的东西。如果跟形式化方法的结合，可以做一些paper出来。自己太懒，没有功夫去follow学术界在这两个方向上的最新潮流，也许有些idea可以借鉴。起码这两个领域比SOA更加实在有趣。也可以考虑在这里做些工程性的东西。

其实formal methods之于计算机科学技术的其他领域，就像数学之于物理。方法和工具是现成的（比如model checking），关键是给自己定义的一大堆符号找到一个合理的解释。大牛可以直接折腾方法论本身，普通人还是老老实实的做application吧。