2011年12月9日星期五

zz 关于g++ memcpy’ was not declared in this scope解决方法

使用如下2行即可
#include<iostream>
#include <cstring>

地址：http://blog.chinaunix.net/u1/38994/showart_2187440.html

2011年12月3日星期六

原文：http://blog.csdn.net/asz9255/article/details/6375281

准备好cuda4.0 64位toolkit,sdk,驱动。注意在安装vs2008时，一定要选择安装64位编译器。如果已经安装了，可在进入维护界面，升级，在VC++里，勾上64编译器。
安装好toolkit,sdk后，跟CUDA3.2一样设置环境变量，我的电脑-》属性-》高级-》环境变量：在系统变量Path的值中加入，……\NVIDIA GPU Computing SDK 3.2\C\bin\win32\Debug和……\NVIDIA GPU Computing SDK 3.2\C\bin\win32\Release（SDK安装路径）。
    大功告成，注销系统，打开VS2008，可以新建CUDA项目了。

编译一个例子，不出意外的话，会报错缺少cutil64。因为CUDA4.0不在包括cutil32和和cutil64，所以我们得人工编译生成。
在......SDK/C/Common中，打开vs2008工程，在32位和64位下，分别在debug和release下重新编译工程，生成的lib在......SDK/C/Common/lib中。
打开VS，在Tool –> Options –> Projects and Solutions –> VC++ Directories 添加刚才生成的两个lib文件。
就是这样！！！

Tool->Options->Projects and Solutions->VC++ Directories

Include files中添加路径（最后）：
....../NVIDIA Corporation/NVIDIA CUDA SDK/common/inc
....../NVIDIA Corporation/NVIDIA GPU Computing SDK 4.0/shared/inc

Library files中添加路径（最后）：
  ....../NVIDIA Corporation/NVIDIA CUDA SDK/common/lib
  ....../NVIDIA Corporation/NVIDIA GPU Computing SDK 4.0/shared/lib

Source files中添加路径（最后）：
  ....../NVIDIA Corporation/NVIDIA CUDA SDK/common/src
....../NVIDIA Corporation/NVIDIA GPU Computing SDK 4.0/shared/src

模板：

CUDA VS Wizard，下载地址：http://sourceforge.net/projects/cudavswizard/files/，有32位和64位两个版本，选择和自己操作系统对应的版本即可，下载后安装

高亮：
F:\。。。\NVIDIA GPU Computing SDK 4.0\C\doc\syntax_highlighting\visual_studio_8

1. If you don't have a usertype.dat file in your "Microsoft Visual Studio 8\Common7\IDE" folder, then copy the included usertype.dat file there. If you do, append the contents of the included usertype.dat onto the end of the "Microsoft Visual Studio 8\Common7\IDE\usertype.dat"

2. Start Visual Studio 8. Select the menu "Tools->Options...". Open "Text Editor" in the tree view on the left, and click on "File Extension". Type cu in the "Extension" box, set the editor to "Microsoft Visual C++" and click "Add". Click "OK" on the dialog box.

3. Restart Visual Studio and your CUDA code should now have syntax highlighting.

无法打开sdk例子的解决办法：
It appears that the CUDA SDK 4.0 Installer may be removing the NvCudaRuntimeApi.rules and CUDA rules files located in the Visual Studio Directory. Someone at NVIDIA will be investigating in detail what exactly is happening during SDK installation. There is a copy of the the *.rules files installed in the CUDA toolkit directory. You can copy the *.rules files from:

C:\Program Files\NVIDIA Corporation\NVIDIA GPU Computing Toolkit\CUDA\r4.0\extras\visual_studio_integration\ rules\*.rules

to

${Your Visual Studio Location}\VC\VCProjectDefaults\

2011年12月2日星期五

MPICH2 + Netbeans

My computer is 64 bit but the linker of Netbeans 7 does not work with mpich2-1.4.1p1-win-x86-64.msi but works with mpich2-1.4.1p1-win-ia32.msi

打开wmpiregister.exe
注册当前用户名和密码

用管理员权限打开cmd
smpd -install

The steps to compile it:

File / New Project … / C/C++ Aplication, name it and go with defaults
Replace content of main.cpp with the code above.
Rightclick on project name on the left, select Properties:

Categories / Build / C++ Compiler -> Include directories add value C:/Program Files (x86)/MPICH2/include
Categories / Build / Linker -> Additional Library Directories add C:/Program Files (x86)/MPICH2/lib
Categories / Build / Linker -> Libraries click “Add Option” and select “Static Bindings” (will add flag -static to the linker)
Categories / Build / Linker -> Add Library ... and select one by one, all .lib files from C:/Program Files (x86)/MPICH2/lib

2011年11月7日星期一

zz eclipse运行C++控制台不输出结果的解决办法

解决方法：

Run Configurations -> Environment

Name

: PATH
Value : C:\MinGW\bin

在运行设置中增加 Path=C:\MinGW\bin

2011年11月4日星期五

ubuntu eclipse c++ cdt 安装

通过Eclipse的Help -> Install New Software进入安装插件界面;
首先，需要添加一个CDT的下载站点，填写CDT的下载地址：
p2 software repository: http://download.eclipse.org/tools/cdt/releases/indigo

之后在此站点安装CDT包即可。

2011年11月3日星期四

Linux下安装MPICH（转载）

Linux下安装MPICH

http://www.cnblogs.com/liyanwei/archive/2010/04/26/1721142.html

Linux 下 mpich2 安装

1：从MPICH2官网下载源代码，http://www.mcs.anl.gov/research/projects/mpich2 /downloads/tarballs/1.0.8/mpich2-1.0.8.tar.gz 目前最新的是1.0.8，当然如果你使用的windows平台也可以下载http://www.mcs.anl.gov/research /projects/mpich2/downloads/tarballs/1.0.8/mpich2-1.0.8-win-ia32.msi，以及 http://www.mcs.anl.gov/research/projects/mpich2/documentation/files/mpich2-1.0.8-windevguide.pdf 这是windows平台下的开发文档。

你也可以登录http://www.mcs.anl.gov/research/projects/mpich2/downloads/index.php?s=downloads，查看你需要的mpich版本，根据自己需要下载即可。

2、然后，将mpich2-1.0.8.tar.gz解压到/home/mpi/mpich2/src中，

执行下列命令：cd /home/mpi/mpich2/src

./configure -prefix=/home/mpi/mpich2(配置安装位置为 /home/mpi/mpich2)

如果没有问题，再运行下面

make

make install

稍等就大功造成了。

3、修改机器的~/.bash_profile（Ubuntu修改~/.bashrc）文件，在最后加上下面的语句

export MPI_ROOT=/home/mpi/mpich2

export PATH=$MPI_ROOT/bin:$PATH

export MANPATH=$MPI_ROOT/man:$MANPATH

4、编辑下面的文件，并存储为hello.c

#include "mpi.h"

#include <stdio.h>

#include <math.h>

int main (int argc, char **argv)

{

int myid, numprocs;

int namelen;

char processor_name[MPI_MAX_PROCESSOR_NAME];





MPI_Init

(&argc, &argv);



MPI_Comm_rank

(MPI_COMM_WORLD, &myid);



MPI_Comm_size

(MPI_COMM_WORLD, &numprocs);



MPI_Get_processor_name

(processor_name, &namelen);

fprintf (stderr, "Hello World! Process %d of %d on %s\n", myid, numprocs, processor_name);



MPI_Finalize

();

return 0;

}

5、接着编译一下

mpicc -o hello hello.c
（ C程序用 mpicc编译，C++程序用mpicxx编译）

6、 MPI应用一个管理器来管理运行MPI程序，这个管理器就是mpd，但是在正式开始运行mpd前还需要一个基于安全考虑的配置文件.mpd.conf，这个文件是要放在运行程序的用户的home目录下，本例子中就是/home/mpi/.mpd.conf，而且这个文件只能由这个用户读写，创建文件的命令是，

cd $HOME
touch .mpd.conf
chmod 600 .mpd.conf
然后在.mpd.conf文件中（如果没有这个文件需要创建一个）写入这么一行，secretword=***，***可以是任意的值，如果配置集群的话，这个值在参与计算的计算机上必需完全一致。如果是root用户的话，这个文件应该是/etc/mpd.conf。

7、启动并行环境 mpdboot
第一次使用这个命令时，可能会出现错误，执行以下代码
cd ～
touch .mpd.conf //这是修改mpd配置文件的时间戳
chmod 600 .mpd.conf //这是修改配置文件的权限

运行程序： mpirun -np 4 ./hello
-np 是指用几个进程模拟运行，这里用4个
输出结果为：（下面结果每台机器可能都不一样，是正常的）
Hello World! Process 1 of 4 on jack-laptop
Hello World! Process 3 of 4 on jack-laptop
Hello World! Process 2 of 4 on jack-laptop
Hello World! Process 0 of 4 on jack-laptop
想停止并行运行环境
mpdcleanup

8、如在第七步出现类似下面的报错

mpdroot: perror msg: Connection refused

mpdroot: cannot connect to local mpd at: /tmp/mpd2.console_root

probable cause: no mpd daemon on this machine

possible cause: unix socket /tmp/mpd2.console_root has been removed

请打开另外一个终端，并执行mpd命令，同时不要关闭这个终端，在执行第7步即可。

9、如果你的os是Ubuntu的话，安装过程中如果提示缺少什么，首先安装这个东西之后再按照这个步骤即可。

2011年10月15日星期六

Ubuntu下eclipse快捷方式找不到JVM的问题（转载：http://blog.csdn.net/seafit/article/details/5673629）

昨日通过vmware装上最新的Ubuntu系统，电脑配置比较高，所以跑起来速度还是很不错。接着装了TOMCAT，ANDROID，等等必须的开发软件。不过期间eclipse的一个问题确实花了不少时间，记录一下解决方案。

1,下载JDK和ECLIPSE。
       下载就不用说了，去eclipse官网下一个伽利略的版本即可，JDK相信下载过WINDOWSjava的人都知道。最好用1.5.0版的，网上说JDK1.6编译android会出问题，我没试过，为了少走弯路，吸取了前人经验。

        安装JDK方面也不用多说，网上资料太多了。这里记录几个细节问题。

        JDK路径：基本上JDK装在任何地方都是可以的，把JAVA_HOME，classpath, path指对路径就可以了，我的安装如下。

         export JAVA_HOME=/usr/java/jdk1.5.0_22
         export CLASSPATH=.:$JAVA_HOME/lib/dt.jar:$JAVA_HOME/lib/tools.jar
         export PATH=$PATH:$JAVA_HOME/bin

          由于我是初学linux，对于linux的环境变量不知道如何设置，从网上的结果来看，我在/etc/bash.bashrc    和 /etc/environment里都加了以上三行。

2，安装eclipse.
          从网上来看，eclipse也是可以安装在任何地方的，我的安装在/opt/eclipse里。安装完成后，会在Applications->program里有一个快捷方式。这下问题就来了，点击这个快捷方式会报下面的错误。

A Java Runtime Environment (JRE) or Java Development Kit (JDK)
must be available in order to run Eclipse. No Java virtual machine
was found after searching the following locations:
/opt/eclipse/jre/bin/java
java in your current PATH

这个就本篇博客要记录的内容，因为这个简单的问题花了我很多时间。
从最后的解决办法来看，是因为桌面启动没有加载之前提到的三行环境变量。但是在控制台是可以通过命令行启动的。

解决办法是在终端进入你的eclipse目录，然后输入：

mkdir jre
cd jre
ln -s 你的JDK目录/bin bin

最后的解决办法如下：

在创建文件 /usr/bin/eclipse 内容如下
#!/bin/sh
export MOZILLA_FIVE_HOME=/usr/lib/mozilla/
export ECLIPSE_HOME=/opt/eclipse

export JAVA_HOME=/usr/java/jdk1.5.0_22
export CLASSPATH=.:$JAVA_HOME/lib/dt.jar:$JAVA_HOME/lib/tools.jar
export PATH=$PATH:$JAVA_HOME/bin

$ECLIPSE_HOME/eclipse $*

然后编辑ECLIPSE的快捷方式
将command 变为 eclipse.

也可以自己写一个bash脚本，我放在了/userrun/eclipse.sh.   内容如下

#!/bin/sh
export GDK_NATIVE_WINDOWS=1
export ECLIPSE_HOME=/opt/eclipse
export JAVA_HOME=/usr/java/jdk1.5.0_22
export CLASSPATH=.:$JAVA_HOME/lib/dt.jar:$JAVA_HOME/lib/tools.jar
export PATH=$PATH:$JAVA_HOME/bin

$ECLIPSE_HOME/eclipse $*

然后把快捷方式的command变为 /userrun/eclipse.sh 也可以实现快捷方式启动eclipase.

网上搜了很多资料，都是零碎的，每个人说几点，但都没有说全，很费解。回头看看还是很简单的，环境变量设置对了就一切搞掂

ubuntu10 Realtek ID 270 无声

Step 1

If you are using Ubuntu 11.04 (Natty), then execute this command and reboot:

sudo add-apt-repository ppa:ubuntu-audio-dev/ppa; sudo apt-get update;sudo apt-get dist-upgrade; sudo apt-get install linux-sound-base alsa-base alsa-utils gdm ubuntu-desktop  linux-image-`uname -r` linux-alsa-driver-modules-$(uname -r) libasound2; sudo apt-get -y --reinstall install linux-sound-base alsa-base alsa-utils gdm ubuntu-desktop  linux-image-`uname -r` linux-alsa-driver-modules-$(uname -r)  libasound2; killall pulseaudio; rm -r ~/.pulse*

If you are using Ubuntu 10.10 (Maverick), then execute this command and reboot:

sudo add-apt-repository ppa:ubuntu-audio-dev/ppa; sudo add-apt-repository ppa:ricotz/unstable;  sudo apt-get update;sudo apt-get dist-upgrade; sudo apt-get install  linux-sound-base alsa-base alsa-utils gdm ubuntu-desktop  linux-image-`uname -r` linux-alsa-driver-modules-$(uname -r) libasound2; sudo apt-get --reinstall install  linux-sound-base alsa-base alsa-utils gdm ubuntu-desktop  linux-image-`uname -r` linux-alsa-driver-modules-$(uname -r) libasound2; killall pulseaudio; rm -r ~/.pulse*

If you are using Ubuntu 10.04 (Lucid), then execute this command and reboot:

sudo add-apt-repository ppa:ubuntu-audio-dev/ppa; sudo add-apt-repository ppa:team-iquik/alsa; sudo apt-get update; sudo apt-get dist-upgrade; sudo apt-get install linux-sound-base alsa-base alsa-utils gdm ubuntu-desktop linux-image-`uname -r` linux-alsa-driver-modules-$(uname -r) libasound2; sudo apt-get --reinstall install linux-sound-base alsa-base alsa-utils gdm ubuntu-desktop linux-image-`uname -r` linux-alsa-driver-modules-$(uname -r)  libasound2; killall pulseaudio; rm -r ~/.pulse*

If you are using Ubuntu 9.10 (Karmic), then you should upgrade to Ubuntu 10.04.2 LTS or newer versions. End of life date for Ubuntu 9.10 was April 2011.

If you upgraded ALSA using the command above and still do not have working sound after rebooting your PC again, then execute this command, reboot and retest sound using headphones and speakers:

cd; sudo apt-get update; sudo apt-get -y install build-essential ncurses-dev gettext xmlto libasound2-dev linux-headers-`uname -r` libncursesw5-dev; wget ftp://ftp.alsa-project.org/pub/driver/alsa-driver-1.0.24.tar.bz2; tar jxvf ./alsa-driver-1.0.24.tar.bz2; rm ./alsa-driver-1.0.24.tar.bz2; cd ./alsa-driver-1.0.24; sudo ./configure; sudo make; sudo make install; killall pulseaudio; cd; rm -r ~/.pulse*; rm ./alsa-driver-1.0.24

Step 2

In gnome-terminal, make sure that unlimited scrolling is enabled:

click on Edit > Profiles > "Default" profile > Scrolling. Choose "Unlimited" as scrolling option. Click Close and Close again.

If you are using the Gnome interface, open the Terminal console via "Applications->Accessories->Terminal"

If you are using the Unity interface, the easiest way to open the Terminal is to use the 'search' function on the dash. Or you can click on the 'More Apps' button, click on the 'See more results' by the installed section, and find it in that list of applications. A third way, available after you click on the 'More Apps' button, is to go to the search bar, and see that the far right end of it says 'All Applications'. You then click on that, and you'll see the full list. Then you can go to Accessories > Terminal after that.

So the methods in Unity are:

Dash > Search for Terminal

Dash > More Apps > 'See More Results' > Terminal

Dash > More Apps > Accessories > Terminal

Step 3

Reboot your computer. Then run the following 2 diagnostic commands.

Tip: If you have a wheel mouse or 3-button mouse, you do not need to type the commands into the Terminal. Instead, copy the commands from this web page and paste them into the terminal. To do this, move your mouse cursor over the start of the command written on the Web page. Then press the left mouse button and drag the mouse till the end of the command to highlight the whole command; then release the mouse button. Then press the middle mouse button or mouse wheel anywhere inside the Terminal. The command should now be printed in the Terminal without errors. Now press <Enter> to execute the command.

wget -O alsa-info.sh http://www.alsa-project.org/alsa-info.sh; chmod +x ./alsa-info.sh; ./alsa-info.sh

Post the full Terminal output after the script has actually run by creating a new question in launchpad then copy&paste the terminal output into your newly created question. Carefully inspect the Terminal output of the ALSA Information script that was generated by the previous diagnostic command

bash alsa-info.sh --stdout

After upgrading ALSA and rebooting the computer make sure that the ALSA driver version, library version and utilities version are all exactly the same version number.

The Terminal output after running the ALSA information script should contain something like this:

# ALSA Version

# Driver version: 1.0.24

# Library version: 1.0.24.1

# Utilities version: 1.0.24.2

If the Driver, Library and Utilities version numbers are not equal, this probably due to one of the following issues:

1. One of the ALSA components was not successfully upgraded during step 1 in this procedure

2. ALSA was correctly installed or upgraded, but a wrong / old kernel was booted instead of the most recent kernel version. In that case, boot the newest kernel version (that is available in the standard/default Ubuntu repositories) and then retest sound.

For example: if you installed or upgraded to Ubuntu 10.10 (Maverick Meerkat edition), make sure the running kernel version is 2.6.35-22-generic or higher. Or else sound will not work!

For example: if you installed or upgraded to Ubuntu 10.04 (Lucid Lynx edition), make sure the running kernel version is 2.6.32-21-generic or higher. Or else sound will not work!

Step 4

Copy & paste the following diagnostic command into the Linux Terminal, then press <Enter>. The command starts with the command cat and ends with the word sound. (Do not copy & paste this diagnostic command from an email message into the Terminal, as that will only copy part of the command.) When asked for your password, type your normal user password (no stars are given as you type); then press <Enter> again.

cat /proc/asound/{version,cards,devices,hwdep,pcm,seq/clients}; sudo rm /etc/asound.conf; sudo rm -r ~/.pulse ~/.asound* ;sudo rm ~/.pulse-cookie; sudo apt-get update; sudo apt-get install aptitude; sudo aptitude install paman gnome-alsamixer libasound2-plugins padevchooser libsdl1.2debian-pulseaudio; sudo lshw -short;ls -lart /dev/snd;  cat /dev/sndstat; lspci -nn;  sudo which alsactl; sudo fuser -v /dev/dsp /dev/snd/* ; dpkg -S bin/slmodemd; dmesg | egrep 'EMU|probe|emu|ALSA|alsa|ac97|udi|snd|ound|irmware'; sudo /etc/init.d/sl-modem-daemon status; sudo grep model /etc/modprobe.d/* ; sudo dmidecode|egrep 'anufact|roduct|erial|elease'; lsmod | egrep 'snd|usb|midi|udio'; aplay -l; sudo lshw -C sound

Your ALSA output shows several issues:
Step A)
WARNING: All config files need .conf: /etc/modprobe.d/alsa-base, it will be ignored in a future release.
WARNING: All config files need .conf: /etc/modprobe.d/options, it will be ignored in a future release.
Please run the following commands to delete those invalid ALSA configuration files:
sudo rm /etc/modprobe.d/alsa-base
sudo rm /etc/modprobe.d/options
Only the following configuration file is the right one to use in Ubuntu 10.04 and should NOT be deleted:
/etc/modprobe.d/alsa-base.conf
Step B)
!!ALSA Version
!!------------
Driver version: 1.0.21
Library version: 1.0.22
Utilities version: 1.0.22
Your ALSA driver, library and utilities versions are not equal and not fully up-to-date.
Please execute the following procedure to upgrade ALSA to version 1.0.23:
http://monespaceperso.org/blog-en/2010/05/02/upgrade-alsa-1-0-23-on-ubuntu-lucid-lynx-10-04/
Step C)
!!Modprobe options (Sound related)
!!--------------------------------
snd-pcsp: index=-2
snd-hda-intel: model=m51va
!!HDA-Intel Codec information
!!---------------------------
--startcollapse--
Codec: Realtek ID 270
The model option you selected to use in /etc/modprobe.d/alsa-base.conf does not correspond with the Codec version that the ALSA driver detected. Codec: Realtek ID 270 means that your ALSA driver is unable to identify precisely which Codec and mixer type is linked to your soundcard. This is another reason to upgrade ALSA to a newer version. Hopefully, the newer ALSA driver can correctly identify the Codec.
So there is no good reason YET to set a model option in the /etc/modprobe.d/alsa-base.conf file.
Run the following command:
gksudo gedit /etc/modprobe.d/alsa-base.conf
In the /etc/modprobe.d/alsa-base.conf file, REMOVE the following line, if it exists:
options snd-hda-intel model=m51va
Then save the change to the file.
After executing steps A, B and C, please reboot and retest sound.

ubuntu 开机自动运行命令

cd /etc
sudo gedit rc.local
在其中加入命令最后要以 exit 0 结束

2011年10月14日星期五

安装Ubuntu Fcitx (转载）

安装Ubuntu Fcitx

sudo apt-get install im-switch fcitx   
sudo im-switch -s fcitx -z default  
im-switch -s fcitx -z default #修改当前用户的默认输入法, 具体看man im-switch

Ubuntu Fcitx完成设置最好重启一下X，输入法就生效了.如果发现软件界面字体是方块,gedit ~/.fcitx/config或gksu gedit /usr/share/fcitx/data/tables.conf打开配置文件修改一下字体就OK.可以使用fc-list来查看已安装的字体。如果配置文件出现乱码，使用gedit --encoding gbk XXX #打开配置文件。
Ubuntu Fcitx 字体列表: xlsfonts或 fc-list (取=前面)
某些情况下可能，在安装了fcitx输入法以后可能会出现和SCIM并存的问题，只要用im-switch把默认输入法改成fcitx就可以了：

sudo im-switch -a fcitx  
im-switch -a fcitx

Ubuntu Linux 10.04自带的输入法不是很好用，linux下的输入法和windows下的比起来还是有很大差距的，相对来说比较好的输入法我看还是fcitx还不错，不过在Ubuntu下通过“sudo apt-get install fcitx”命令安装之后会出现方块的乱码。那是因为fcitx安装后默认的中文显示字体设置错误。
fcitx的配置文件是~/.fcitx/config
但是直接用 gedit ~/.fcitx/config 打开配置文件显示的也都是乱码，解决办法就是指定编码方式打开“sudo gedit --encoding gbk ~/.fcitx/config” Ubuntu默认的编码方式是UTF-8格式，因此需要通过gbk方式来打开该文件。

[程序]
显示字体(中)=*
显示字体(中)=*
显示字体 (英)=Courier New
显示字体(英)=Courier New
显示字体大小=12
主窗口字体大小=9
字体区域=zh_CN.UTF-8
使用AA字体=1
使用粗体=1
使用托盘图标=1

需要将第一行配置改成

“显示字体(中)=AR PL ShanHeiSun Uni”

注销之后，fcitx正常工作。

ubuntu compaq wireless driver network unclaimed---from others

network UNCLAIMED in wireless on ubuntu 9.10 Can anyone tell me how to find wireless network drivers for ubuntu 9.10 on Compaq 510 notebook. Here is the output of "lshw -C network" -network UNCLAIMED description: Network controller product: Realtek Semiconductor Co., Ltd. vendor: Realtek Semiconductor Co., Ltd. physical id: 0 bus info: pci@0000:10:00.0 version: 10 width: 32 bits clock: 33MHz capabilities: bus_master cap_list configuration: latency=0 resources: ioport:6000(size=256) memory:e8000000-e8003fff -network description: Ethernet interface product: Marvell Technology Group Ltd. vendor: Marvell Technology Group Ltd. physical id: 0 bus info: pci@0000:30:00.0 logical name: eth0 version: 10 serial: 18:a9:05:d2:e5:0c width: 64 bits clock: 33MHz capabilities: bus_master cap_list ethernet physical configuration: broadcast=yes driver=sky2 driverversion=1.23 firmware=N/A ip=192.168.1.2 latency=0 multicast=yes resources: irq:29 memory:e0000000-e0003fff ioport:2000(size=256) lspci -nn 00:00.0 Host bridge [0600]: Intel Corporation Mobile GME965/GLE960 Memory Controller Hub [8086:2a10] (rev 0c) 00:02.0 VGA compatible controller [0300]: Intel Corporation Mobile GME965/GLE960 Integrated Graphics Controller [8086:2a12] (rev 0c) 00:02.1 Display controller [0380]: Intel Corporation Mobile GME965/GLE960 Integrated Graphics Controller [8086:2a13] (rev 0c) 00:1a.0 USB Controller [0c03]: Intel Corporation 82801H (ICH8 Family) USB UHCI Controller #4 [8086:2834] (rev 03) 00:1a.7 USB Controller [0c03]: Intel Corporation 82801H (ICH8 Family) USB2 EHCI Controller #2 [8086:283a] (rev 03) 00:1b.0 Audio device [0403]: Intel Corporation 82801H (ICH8 Family) HD Audio Controller [8086:284b] (rev 03) 00:1c.0 PCI bridge [0604]: Intel Corporation 82801H (ICH8 Family) PCI Express Port 1 [8086:283f] (rev 03) 00:1c.1 PCI bridge [0604]: Intel Corporation 82801H (ICH8 Family) PCI Express Port 2 [8086:2841] (rev 03) 00:1c.4 PCI bridge [0604]: Intel Corporation 82801H (ICH8 Family) PCI Express Port 5 [8086:2847] (rev 03) 00:1c.5 PCI bridge [0604]: Intel Corporation 82801H (ICH8 Family) PCI Express Port 6 [8086:2849] (rev 03) 00:1d.0 USB Controller [0c03]: Intel Corporation 82801H (ICH8 Family) USB UHCI Controller #1 [8086:2830] (rev 03) 00:1d.1 USB Controller [0c03]: Intel Corporation 82801H (ICH8 Family) USB UHCI Controller #2 [8086:2831] (rev 03) 00:1d.2 USB Controller [0c03]: Intel Corporation 82801H (ICH8 Family) USB UHCI Controller #3 [8086:2832] (rev 03) 00:1d.7 USB Controller [0c03]: Intel Corporation 82801H (ICH8 Family) USB2 EHCI Controller #1 [8086:2836] (rev 03) 00:1e.0 PCI bridge [0604]: Intel Corporation 82801 Mobile PCI Bridge [8086:2448] (rev f3) 00:1f.0 ISA bridge [0601]: Intel Corporation 82801HEM (ICH8M) LPC Interface Controller [8086:2815] (rev 03) 00:1f.1 IDE interface [0101]: Intel Corporation 82801HBM/HEM (ICH8M/ICH8M-E) IDE Controller [8086:2850] (rev 03) 00:1f.2 SATA controller [0106]: Intel Corporation 82801HBM/HEM (ICH8M/ICH8M-E) SATA AHCI Controller [8086:2829] (rev 03) 10:00.0 Network controller [0280]: Realtek Semiconductor Co., Ltd. Device [10ec:8171] (rev 10) 30:00.0 Ethernet controller [0200]: Marvell Technology Group Ltd. Device [11ab:4357] (rev 10) Your Realtek uses the driver r8192se_pci. You will need to get an ethernet connection and get some files from the internet: Code: sudo apt-get install linux-headers-generic build-essential Then go here: http://ubuntuforums.org/showpost.php...55&postcount=5 You can follow each step carefully and even copy and paste his commands into a terminal. There is one correction, however, his two commands that start with 'sed' should be run as sudo; that is, sudo sed ...etc. You should then disconnect the wire and click the Network Manager icon and connect wirelessly. rtl8192se - Wireless Problems on 1201N I found a solution to get wireless networking to work without NDISWrapper! I went to the following link to figure it out: https://bugs.launchpad.net/ubuntu/+s...6?comments=all I used the rtl8192se_linux_2.6.0010.1211.2009.tar.gz file which was referenced in post #134 and is available here: http://launchpadlibrarian.net/366886...11.2009.tar.gz I did the following to get it to work after downloading the file: Code: tar xzf rtl8192se_linux_2.6.0010.1211.2009.tar.gz cd rtl8192se_linux_2.6.0010.1211.2009 sudo make Then you need to edit two files to work with Ubuntu using the following commands (This works on Ubuntu 9.10): Code: sed -i 's/install: modules/install:/g' ./ieee80211/Makefile sed -i 's/install: modules/install:/g' ./HAL/rtl8192/Makefile Then you install with the following command: Code: sudo make install sudo echo "r8192se_pci" > /etc/modules sudo modprobe r8192se_pci

linux关闭手写板 ----转载

打字的时候，如果不小心碰到触摸板，鼠标一下子不知道飞哪去了，真的是让人挺烦恼的一件事情。
解决方法如下

1.终端输入如下命令：
sudo modprobe -r psmouse
如果打开触摸板就是：
sudo modprobe psmouse

注：此方法重启系统后触摸板又会自动激活。%>_<%

2.最近我又重新安装了一次Ubuntu9.10，发现在鼠标设置那有个“打字时禁用触摸板”，点上以后打字的时候即使碰到触摸板，光标也不会丢了。O(∩_∩)O~

要是想永久禁用触摸板可以参考一下方法：

安装gsynaptics软件包，系统菜单中会出现“触摸板”的选项。
命令:sudo apt-get install gsynaptics

然后在 “系统－－>首选项－－>触摸板－－>一般－－>启用触摸板”，去选该项就可以一劳永逸地禁用恼人的触摸板了。方法是网上找的.本人测试此方法不行,关闭后一段时间触摸板会自动启动,权限的问题

3.最好的方式还是通过脚本实现吧。方法如下：（此方法自己想的，不可行啦，无法完成自启动，有待改进！）
创建脚本文件：
命令：vi closeTouchpad.sh
（如果不想让脚本文件显示，可以在文件名前加“.”即可）
内容：
#!/bin/sh
if xinput list-props "SynPS/2 Synaptics TouchPad" | grep "Device Enabled" | grep 1
then
modprobe -r psmouse
else
modprobe psmouse
fi
给脚本文件加上可执行权限：chmod +x closeTouchpad.sh
将脚本文件拷贝到任意路径（我的是放到了/usr目录下）：sudo cp closeTouchpad.sh /usr
在/etc/init.d/目录下建立软连接实现自启动：sudo ln -s /usr/closeTouchpad.sh closeTouchpad
这里注意：脚本文件必须是root权限來执行才能生效，所以在/etc/init.d/下建立软链接，当然也可以直接把脚本文件copy到/etc/init.d/里面。
下次启动Ubuntu的时候，脚本就会自动执行关闭触摸板了。注意出门别忘带鼠标，如果忘记只能在终端执行
sudo modprobe psmouse 來启用触摸板了，怎么键盘启动终端，自己想想办法吧。

2011年7月19日星期二

freebox 用 vlc 看电视

如果用 IE 看14套低频节目话可以用
http://tv.freebox.fr/

如果用 VLC 看, 可以用
http://mafreebox.freebox.fr/freeboxtv/playlist.m3u9 m0 P$ i% }' u' O) e+ B
; n* M4 o  R9 O) s9 L/ R. k# `

如果想容易记住节目表链接.5 G% n( b  x* m/ U3 k9 f1 ~
有下面的方法:6 ~/ i* c9 u) R' ~( {
1- 把它记在一个小文档里, 每次打开它, coller-copier.
2-  在VLC, 菜单 "Paramètres" - "Préférences"  - "PlayList" -"Général". 在右边, 有个"Flux pardéfaut" (*), 输入 http://mafreebox.freebox.fr/freeboxtv/playlist.m3u 然后点最下面的 "Enregistrer" .1 l! s/ w: }9 C
3 - 用右键点这个链接6 U7 _5 l7 Q+ \
http://mafreebox.freebox.fr/freeboxtv/playlist.m3u9 o6 d9 c! O# Z+ @' k4 H
选"链接另存为" 存到硬碟 (不要选桌面) 后 , 用explorer 找到它, 再用右键点文件 "playlist.m3u" 选"Ouvrir avec ", 在 "Choix de programme", 选 "VLC Media player". 并勾"Toujours utiliser ce programme pour ouvrir ce type de fichier".这样以后每次用滑鼠双击它时, 就会开始放VLC的电视了.
2 e9 y. ~7 S7 l8 h9 ~5 N* v& n
新版本的 VLC, 选偏爱选项, 左边要选全部, 再在媒体播放表设定里输入这个地址.
这样, 以后每次一旦打开 VLC, 它会自动播放.

2011年6月25日星期六

哲学家进餐问题 java

哲学家进餐问题的解决方案主要有以下几种：
（１）利用ＡＮＤ型信号量机制．该方案的思路是，仅当哲学家左右两支筷子都空闲时，才允许他拿起筷子进餐，即哲学家所需要的临界资源──筷子，要么两支全部分配给他，要么一支都不分配，这样就保证了总有哲学家能同时拿到两支筷子而进餐，当他进餐完毕释放筷子后，其他哲学家也可以顺利地运行下去，避免了死锁的产生．
（２）对哲学家按序号进行区分．该方案的思路是，让第０、２、４号哲学家先去申请他们左手边的筷子（即第０、２、４号筷子），然后再去申请右手边的筷子，让第１、３号哲学家先申请他们右手边的筷子（即第２、４号筷子），然后再申请左手边的筷子．这样总会有一名哲学家能够同时拿到两支筷子而进餐，当他进餐完毕，释放其左右手的筷子后，其他哲学家又能继续下去，从而确保每位哲学家都可以顺利地进餐．
（３）最多允许４名哲学家提出申请．该方案的思路是，至多允许４名哲学家提出进餐申请，以保证至少有１名哲学家能够拿到两支筷子而进餐，他最终总会释放出所使用的两支筷子，从而使其余哲学家可以进餐．
（4）回退思想的引入回退机制的理论依据是处理死锁基本方法中的预防死锁策略．预防死锁是指通过设置某些限制条件，去破坏产生死锁的４个必要条件中的一个或几个来防止死锁的发生．其中“摒弃不剥夺条件”规定，当一个进程提出新的资源请求而不能立即得到满足时，必须释放其已经保持了的所有资源，即已经占有的资源可以被剥夺．根据上面的理论，本文解决哲学家进餐问题的基本思路是，让每名哲学家先去申请他左手边的筷子，然后再申请他右手边的筷子，如果右手边的筷子不空闲，则比较当前哲学家i 和他右手边的哲学家（i ＋１）％５，看谁取得各自左手边筷子的时间更晚，令其回退（即释放左手筷子，再重新申请左手筷子），直到此哲学家右手边的筷子空闲为止．通过设置回退机制，可以确保每位哲学家都能顺利进餐．

同步和死锁的关系要搞清楚：

同步是为了保护多线程对共享数据的访问，消除数据腐蚀。同步的过程中可能会产生死锁！

也就是说，会产生死锁的程序中，共享数据得到了保护，只是程序会死锁。

我的方案：最后一个人先拿左筷，其他人都先拿右筷。（破坏死锁链）
/*
* To change this template, choose Tools | Templates
* and open the template in the editor.
*/
package tr52_java;

import java.util.Random;
import java.util.logging.Level;
import java.util.logging.Logger;

public class Philosopher extends Thread {

    private static int MAX_PHILO = 4;
    private int num;
    private ChopStick right, left;
    private boolean finished = false;
    private Random rand = new Random();
    private boolean flag = true;

    public Philosopher(int i, ChopStick r, ChopStick l) {
        num = i;
        right = r;
        left = l;
        start();
    }

    public void pause() {
        try {
            sleep(rand.nextInt(1000));
        } catch (Exception e) {
            e.printStackTrace();
        }
    }

//会死锁！死锁点在synchronized(left)
//    @Override
//    public void run() {
//        while (!finished) {
//            flag = true;
//            synchronized (right) {
//                while (!right.isFree()) {
//                    try {
//                        right.wait();
//                    } catch (InterruptedException ex) {
//                        Logger.getLogger(Philosopher.class.getName()).log(Level.SEVERE, null, ex);
//                    }
//                }
//                pause();
//                synchronized (left) {
//                    while (!left.isFree()) {
//                        flag = false;
//                        right.notify();
//                        System.out.println(num + "is thinking");
//                        break;
//                    }
//                    if (flag) {
//                        right.take();
//                        System.out.println(num + ": right taking");
//                        pause();
//
//                        left.take();
//                        System.out.println(num + ": left taking");
//                        pause();
//
//                        System.out.println(num + ": eating");
//
//                        right.release();
//                        right.notifyAll();
//                        System.out.println(num + ": right releasing");
//                        pause();
//
//                        left.release();
//                        left.notifyAll();
//                        System.out.println(num + ": left releasing");
//                        pause();
//                    }
//                }
//            }
//        }
//    }
    @Override
    public void run() {
        while (!finished) {
            System.out.println(num + "is thinking");
            synchronized (right) {
                while (!right.isFree()) {
                    try {
                        right.wait();
                    } catch (InterruptedException ex) {
                        Logger.getLogger(Philosopher.class.getName()).log(Level.SEVERE, null, ex);
                    }
                }
                right.take();
                System.out.println(num + ": right taking");
                pause();
            }

            synchronized (left) {
                while (!left.isFree()) {
                    try {
                        left.wait();
                    } catch (InterruptedException ex) {
                        Logger.getLogger(Philosopher.class.getName()).log(Level.SEVERE, null, ex);
                    }
                }
                left.take();
                System.out.println(num + ": left taking");
                pause();
            }

            System.out.println(num + ": eating");

            synchronized (right) {
                right.release();
                right.notifyAll();
                System.out.println(num + ": right releasing");
                pause();
            }

            synchronized (left) {
                left.release();
                left.notifyAll();
                System.out.println(num + ": left releasing");
                pause();
            }
        }
    }

//    @Override
//    public void run() {
//        while (!finished) {
//            right.take();
//            pause();
//            left.take();
//            pause();
//            left.release();
//            pause();
//            right.release();
//            pause();
//        }
//    }
public static void main(String[] args) {
        ChopStick[] chopStick = new ChopStick[MAX_PHILO];
        for (int i = 0; i < MAX_PHILO; i++) {
            chopStick[i] = new ChopStick(i);
        }

        Philosopher[] phil = new Philosopher[MAX_PHILO];
        for (int i = 0; i < MAX_PHILO; i++) {
            if (i < MAX_PHILO - 1) {
                phil[i] = new Philosopher(i, chopStick[i], chopStick[i > 0 ? i - 1 : MAX_PHILO - 1]);
            } else {
                phil[i] = new Philosopher(i, chopStick[i - 1], chopStick[i]);


}
        }
    }
}

class ChopStick {

    private int num;
    private boolean free = true;

    public ChopStick(int i) {
        num = i;
    }

//方案1：
    public void take() {
        free = false;
    }

    public boolean isFree() {
        return free;
    }

    public void release() {
        free = true;
    }
//    public synchronized void take() {
//        free = false;
//    }
//
//    public boolean isFree() {
//        return free;
//    }
//
//    public synchronized void release() {
//        free = true;
//    }
}

2011年6月23日星期四

(转载）用latex和beamer做幻灯片

原文地址：http://xiang.blog.edu.cn/2008/157618.html
做幻灯片是一件头疼的事。而用latex做幻灯片是一件很头疼、很头疼、cdots、很头疼的事……总结和收集了一些经验如下：

beamer教程
有很多教程。对于初学者，最好先copy别人（比如师兄师姐的）模板用，或者直接看beamer的例子，C:CTeXtexmfdoclatexbeamerexamples。入门后，我觉得最好的提高教程是Ki-Joo Kim的Beamer v3.0 Guide，本身就是一个幻灯片，写的很清楚，看得也很爽。最后是beamer的用户手册，参考用。

中文幻灯片
一定要定义documentclass[cjk]{beamer}，别忘了“cjk”，否则编译不通过

pdf书签中文乱码
这是做中文幻灯片时必然遇到的问题……

在Adobe Reader中，显示在一旁的书签(Bookmark)是Unicode的。这样一来，如果单纯是使用pdflatex生成pdf将会显示乱码。所以，若要生成中文的Bookmark就需要执行如下命令:

pdflatex slide.tex
pdflatex slide.tex
gbk2uni slide.out
pdflatex slide.tex

注：gbk2uni是cct的一个小工具。

改变文字颜色
textcolor{blue!80!white}可以调色，这是xcolor包的一个功能。
在WinEdt中要查看任何一个package的用户手册，可以在菜单中选Help-Latex doc，然后输入包名即可。

lyx：可见即所得的Latex编辑器
每个 frame里几乎都要敲一遍begin{itemize}end{itemize；思考若干秒后决定再敲一遍（因为要缩进其中的几个item）；再思考若干秒后把刚敲的这两行删掉（取消缩进）……用beamer就是这么痛苦。想想powerpoint，只要按Tab和Shift+Tab……于是我装了Lyx。虽然它其实还是很难用。下面是Lyx的几个经验：
- 导入中文latex源文件前，应在latex源文件中写usepackage[gbk]{inputenc}指定编码，否则导入后是乱码
- Document-preferences-language改为中文，否则查看源码时有很多解码错误
- 总的来说，还是不建议用Lyx，没有想像中得那么好。

WinEdt宏
为了从上面描述的重复劳动中解脱出来，我花了点时间看了看WinEdt的宏语言手册，写了几个简单的宏，发现还是挺好用的。
- 为当前选中的文本增加一层itemize环境： BeginGroup;
  GetSel(0,1);
  CMD("Delete");
  Ins("begin{itemize}");
  NewLine;
  Ins("%!1");
  NewLine;
  Ins("end{itemize}");
  NewLine;
  EndGroup;
  
  原理很简单，把当前选中文本保存到变量%!1中，删除当前文本，然后插入适当的文本。
- 删除当前选中文本最外层的itemize环境：
  
  DelLabel("","begin{itemize}","end{itemize}");
  就这一行。注意，一定要保证当前选中的文本中的头尾刚好是一对begin{itemize}和end{itemize}。
- 自动插入任意的环境
  
  GetString("Input environment name:","Surround By"); // input string is saved in %!?
  BeginGroup;
  GetSel(0,1); // save current selection in %!1
  CMD("Delete");
  Ins("begin{%!?}");
  NewLine;
  Ins("%!1");
  NewLine;
  Ins("end{%!?}");
  IfStr('%!1','','=', "CMD('Line Up')", 'Relax'); // move one line up if current selection is empty (i.e. inserting a new environment)
  EndGroup;
  
  这个宏首先会提示你输入环境名，然后自动在当前选中的文本前后插入begin{xxx}和end{xxx}。
- 安装宏的方法
  
  Help-Macro Manual，第一页就讲了这个，配了图，可能比我说的更清楚。不过这里还是大致说一下：首先把上面几个宏分别保存为.edt类型的文件，复制到 WinEdt文件夹下面，例如C:CTeXWinEdtMacros。然后在Options-Menu setup-Popup menus里面，选择左边的“Edit”一项，然后按上面的第二个按钮，出现新的对话框，在这里可以修改右键弹出菜单的内容，再按最上面第二个按钮，选 Macro，这样就添加了一个菜单项，给它起个名字”Insert Environment“，然后在Macro编辑框中输入[Exe('%bMacrosInsert Environment.edt');]，确定后即可在右键弹出菜单里用这个新命令了。安装其他宏的方法类似。

总结：自己动手，丰衣足食。其实早就该学一下WinEdt的这些高级功能，可以节约不少时间……

（转载）软件模型检测简介

原文地址：http://blog.csdn.net/xander1981/archive/2009/10/10/4650092.aspx

1. 什么是软件模型检测（software model checking）

a) 软件模型检测是用来在程序执行过程中证明性质正确性的算法。它源于逻辑和定理证明，这两者都给出了基础问题形式化的基本概念，以及提供了分析逻辑问题的算法流程。

b) 随着软件规模的越来越大，使得人工的验证软件变得越来越难，而且人工的验证本身是否可靠也是一个很大的问题。因此，软件模型检测研究的目的就是扩展自动验证技术的应用领域，将其用于程序的推理，无论是在程序处理的验证还是性质的验证上，都要最大程度的增加自动化的比例，从而减轻人，尤其是专家程序员的工作量。

2. 软件模型检测的发展

软件模型检测目前有三方面的发展，这三方面是同时发展的，有其各自的特点：

a) 程序逻辑和相关判定过程【Nelson 1981; Nelson and Oppen 1980; Shostak 1984】的发展给无限状态过程的推理提供了基本框架和基础算法。

b) 基于时序逻辑【Pnueli 1977; Emerson 1990】的自动化模型检测技术【Clarke and Emerson 1981; Queille and Sifakis 1981; Vardi and Wolper 1994】的发展为解决状态爆炸问题提供了基础算法。

c) 通过抽象解释对编译器进行分析和形式化，使得我们在无限状态的逻辑世界空间和有穷状态的算法世界之间建立起了很好的联系。

80年代到90年代期间，这三方面虽然各自有其发展，但是，之间的相互联系却很少。直到最近十几年，现代化的软件模型检测工具成为了研究领域的研究重点，上述三方面的研究也慢慢的结合到了一起。严格意义上来说，“软件模型检测工具”的说法是不太恰当的，因为当前的工具同时具备了定理证明、模型检测、数据流分析等多种传统意义上的程序分析方法。我们保留这一说法的目的是为了反映一个阶段历史的发展。

3. 有形枚举的模型检测（concrete enumerative model checking）

a) 有形（concrete）：方法只关心程序的状态。

b) 枚举（enumerative）：方法的操作对象是程序的单个状态。而符号化（symbolic）的模型检测操作的是状态的集合。

c) 有形枚举的模型检测来源于70年代末期的测试和仿真技术，尤其是对网络协议的测试技术（同一时期，还产生了对时序逻辑进行声明的技术）。之后，该方法被成功的应用在了异步信息传输协议、cache一致性协议等多个领域。

d) 方法介绍：该方法是基于对状态图的搜索遍历，找出所有可达状态的集合，再检查看错误状态是否包含在可达状态集合当中，如果是，则说明系统不安全。否则，说明系统是安全的。

e) 代表性的工具：SPIN【Holzmann 1997】和MURPHI【Dill 1996】。

f) 存在问题：状态爆炸！！！

g) 解决方法：

i. 基于削减的技术（reduction-based techniques）：找出程序行为中的等价关系，并且只考虑每个等价类中的一个成员，保证削减后的是完备的，也即原系统中有的bug，在削减后的系统中同样存在。主要的削减技术有——偏序削减（partial-order reduction）【Valmari 1992; Katz and Peled 1992; Godefroid 1996】，对称削减（symmetry reduction）【Clarke et al. 1993; Emerson and Sistla 1996; Ip and Dill 1996; Sistla et al. 2000】，基于模拟和互模拟的等价类划分来最小化系统【Bouajjani et al. 1990; Loiseaux et al. 1995; Bustan and Grumberg 2003】。

ii. 合成技术（compositional techniques）：将原始的验证问题分解成对其子问题的安全性验证，由子问题安全可以推导出原问题安全。假设-保证推理（assume-guarantee reasoning）【Misra and Chandy 1981; Jones 1983; Stark 1985; Abadi and Lamport 1993; Abadi and Lamport 1995; Henzinger et al. 1998; Alur and Henzinger 1999】是合成推理中发展得比较好的技术。其中还用到了一些启发式的搜索技术来加快对状态空间的搜索，快速的找到系统的问题所在，例如重复加深算法（iterative deepening）【Korf 1985】、最好-优先搜索（best-first search）【Russell and Norvig 2003】、A*算法【Hart et al. 1968; Russell and Norvig 2003】。这些方法在MURPHI和SPIN中也都有了很好的应用。

h) 少量状态搜索（stateless search）

i. 基于深度的限界模型检测。当某一深度的执行路径全部探测完以后没有发现错误就增加深度，再重复这一过程，直到返回UNSAFE，表明发现了与待验证的安全性性质相冲突的执行。该算法的主要特点就是对待分析的程序的表示要求不是很高。我们只要做到两点就可以了：

1. 重置（reset）：对程序的初始状态进行重置；

2. 执行（execute）：在相应的调度策略下执行。

i) 基于执行的工具：

i. Verisoft：最早使用基于执行的少量状态搜索的模型检测软件。能对若干通过消息队列进行通讯的Unix进程进行检测。

ii. JavaPathFinder：对Java程序的模型检测工具。加入了许多常用的基于削减的技术来解决状态爆炸的问题。同时有多种启发式方法来搜索存储的状态空间以及使用一些技术来获得一个更高的覆盖率。

iii. CMC：可以检测C语言程序在执行时，OS层级的调度。

iv. MaceMC：用于检测分布式系统。

v. Chess：用于检测多线程的Windows程序。

4. 有形符号化的模型检测（concrete symbolic model checking）

a) 基于枚举的模型检测技术受到状态和迁移关系数量的影响很明显，很容易产生状态爆炸的问题，因此在实际应用中会遇到很多的困难。这就使得研究者们把目光放在了符号化的模型检测算法上。符号化的模型检测方法是以状态集合为操作对象的，而不是单个单个的状态。符号化的表示方法能够更加简洁的表示系统的状态，而且也能够更好的表示无限状态的集合。为了能够进行验证，符号化的表示方法所表示出来的状态集合还要能够支持必要的运算操作，例如求状态集合的后继、前驱，状态集合的合并等等。

b) 符号化的模型检测算法的基本搜索过程和枚举的模型检测算法的搜索过程类似，只是我们现在操作的对象是状态集合（或者说是区域，region）而不是单个独立的状态。符号化的模型检测方法之所以有效的另外一个原因就是有强有力的可满足性求解工具作其后盾，如SAT【Silva and Sakallah 1996; Moskewicz et al. 2001; Een and Sorensson 2003】，BDD【Bryant 1986; Somenzi 1998】，以及SMT【Dutertre and Moura; Bruttomesso et al. 2008; de Moura and Bjørner 2008】。

c) 符号化的表示方法

i. 命题逻辑：SAT，BDD。

ii. 带有解释定理的一阶逻辑：SMT。

d) 限界模型检测【Biere et al. 1999】

i. 有限步的展开程序控制流程图，检查在该步数内能够找到错误状态，若找到，则返回系统不安全的信息，若找不到，则增加步数，直到步数到达上界，此时返回找不到错误状态的信息。

ii. 对软件的限界模型检测工具又可以分为两类：

1. 用命题逻辑生成约束，通过SAT求解器来求解：CBMC【Kroening et al.2003】，F-Soft【Ivancic et al. 2008】，Saturn【Xie and Aiken 2005】，Calysto【Babic and Hu 2008】。

2. 用适当的一阶理论来生成约束，用SMT求解器来求解。

iii. 限界模型检测适合于查错，即在规定步数内找到系统的错误状态。若系统是安全的，则限界模型检测无法给出完备的判定。我们可以采用其它的方法来解决对系统安全性的判定，如k-induction【Sheeran et al. 2000; de Moura and Ruess 2003】。k-induction是假设归纳不变式在程序执行路径前k步都是成立的，然后证明该不变式在k+1步时同样成立。其中，长度为k的路径是按照限界模型检测的方法进行编码的。这种基于不变式的约束式求解方法受到两方面的限制：1.要猜测出正确的不变式；2.方法的效率受制于求解非线性算术表达式的求解器的效率。因此，这种方法目前只适用于规模较小的程序的验证。

5. 模型检测和抽象技术

a) 对于无限状态的程序来说，符号化的可达性分析同样不能终止，或者是说要花费难以估量的时间和空间代价才有可能终止。抽象模型检测的可达性分析是在抽象域的基础上进行的，而抽象域则是通过抽象语义对程序的运行进行适当的信息捕获而得到的【Cousot and Cousot 1977】。好的抽象域和抽象语义的选择可以很好的保证算法的可靠性和有效性。

b) 基于抽象的可达状态分析

该算法和符号化的可达状态分析算法类似，只是用抽象域代替了符号化的状态集合。根据抽象对象的不同，也有不同的抽象方法：

1. 谓词抽象：【Agerwala and Misra 1978; Graf and Saïdi 1997; Saïdi and Shankar 1999; Das et al. 1999】，代表工具：SLAM，BLAST【Beyer et al. 2007a】。Cartesian谓词抽象技术【Ball et al. 2001】是其中的代表，在系统开销和求解效率上取得了很好的平衡，并且在SLAM中关于C程序验证的部分有其相关的使用，叫做c2bp【Ball et al. 2001】。

2. 控制抽象：流敏感，流不敏感，路径敏感等【Beyer et al. 2007b】。主要是针对非递归的并发程序进行抽象，抽象成顺序执行的程序进行验证【Dwyer and Clarke 1994】。代表工具：MAGIC【Chaki et al. 2004】。

3. 各种抽象技术相结合：结合多种抽象技术，对系统的不同性质进行抽象爱那个，得到一个更加强大的分析工具。代表工具：F-Soft【Jain et al. 2006】，IMPACT【McMillan 2006】，Astree analysis tool【Blanchet et al. 2002; Blanchet et al. 2003】，BLAST。

若基于抽象的可达性分析算法返回safe，则表示原系统真的是安全的；若返回unsafe，则无法判定原系统到底是safe还是unsafe的，因为在抽象的过程中省略掉了一部分信息，有可能原系统是安全的，而在抽象后的系统中却形成伪反例（不完备）。这就需要根据某些信息对抽象后的系统进行修正。基于反例的抽象修正（counterexample guided abstraction refinement）就是其中之一。

6. 抽象修正技术

a) 通常来说，抽象的模型检测技术是可靠的，也即抽象系统是安全的可以推出原系统也是安全的，但是抽象的模型检测方法是不完备的，也即在原系统是安全的情况下，抽象系统有可能会得到一个错误的反例。因此，我们需要判断哪些反例是真的，即在原系统中存在的，哪些反例是假的，即在原系统中不可能存在的。出现后一种情况时，我们希望模型检测算法能够自动的修正，得到一个新的抽象域重新进行检测。这种修正有可能是基于找到的伪反例（counterexample-guided refinement）【Ball and Rajamani 2000b; Clarke et al. 2000; Saidi 2000】，也有可能是其它的策略，例如：局部削减（localization reduction）【Kurshan 1994; Alur et al. 1995】。

上图为CEGAR算法描述。算法不断的修正抽象域A，知道证明系统是正确的，或者找到真正的反例为止。

b) 反例和修正

i. 反例：一条程序执行路径，其第一个状态为系统的初始状态，最后一个状态为一个错误状态。表明程序可以执行到一个错误状态，也即系统安全的一个反例。

ii. 基于语法的修正

1. 一个简单的排出伪反例的方法是查找公式中的不可满足的核心（unsatisfiable core）。有很多方法可以找到这个公式的集合：

a) 用贪心算法找最小不可满足集合，SLAM中用到了该方法【Ball and Rajamani 2002a】；

b) 查询判定的产生过程，找到证明不可满足的那些约束，选择该证明中那些在叶子节点出现的原子公式即可。该方法在BLAST中有实现【Henzinger et al 2002】。

2. 另外一种基于语法的修正方法是计算路径的前驱，即从错误的状态开始，往前计算每一步的状态，并根据计算出的状态中的原子命题进行修正，直至到达初始状态【Namjoshi and Kurshan 2000】。该方法在F-Soft中有应用。

iii. 基于插值的修正

基于语法的修正，往往只关注程序表面的一些问题，而没有考虑其内在的联系。而基于插值的方法则不同，【Henzinger et al. 2004】利用Craig插值（Craig Interpolation）来查找能够反映程序内在联系的断言，来验证给定的安全性性质。

iv. 基于抽象-修正的模型检测工具

1. SLAM【Ball and Rajamani 2002b】

2. BLAST【Beyer et al. 2007a】

3. MAGIC【Chaki et al. 2003】

4. F-Soft【Ivancic et al. 2005】

订阅：博文 (Atom)

火星TNT